From 389d13028b3d55b47a54d1988ae9b45d451ce459 Mon Sep 17 00:00:00 2001
From: Samuel Balco <goodlyrottenapple@gmail.com>
Date: Fri, 28 Jul 2023 12:47:35 +0100
Subject: [PATCH] Fail when checking definition with Z3 returns Unknown (#3628)

Fixes #3619
The definition provided in the above issue now throws the following
error after re-trying once with quadruple the smt timeout:

```
kore-rpc: [4462799] Error (ErrorException):
    The definitions sent to the solver may not be consistent (Z3 timed out).
    CallStack (from HasCallStack):
      error, called at src/Kore/Rewrite/SMT/Lemma.hs:180:9 in kore-0.60.0.0-inplace:Kore.Rewrite.SMT.Lemma
```
---
 kore/src/Kore/Rewrite/SMT/Lemma.hs | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/kore/src/Kore/Rewrite/SMT/Lemma.hs b/kore/src/Kore/Rewrite/SMT/Lemma.hs
index bcb3d4e274..3ba461d678 100644
--- a/kore/src/Kore/Rewrite/SMT/Lemma.hs
+++ b/kore/src/Kore/Rewrite/SMT/Lemma.hs
@@ -24,6 +24,7 @@ import Control.Monad.Except
 import Control.Monad.State qualified as State
 import Data.Functor.Foldable qualified as Recursive
 import Data.Generics.Product.Fields
+import Data.Limit (Limit (..))
 import Data.Map.Strict qualified as Map
 import Data.Text qualified as Text
 import Kore.Attribute.Axiom qualified as Attribute
@@ -52,8 +53,10 @@ import SMT (
     MonadSMT (..),
     Result (..),
     SExpr (..),
+    TimeOut (..),
     assert,
     check,
+    localTimeOut,
  )
 
 getSMTLemmas ::
@@ -84,9 +87,22 @@ declareSMTLemmas ::
 declareSMTLemmas tools lemmas = do
     declareSortsSymbols $ smtData tools
     mapM_ declareRule lemmas
-    isUnsatisfiable <- fmap (Unsat ==) <$> SMT.check
-    when (fromMaybe False isUnsatisfiable) errorInconsistentDefinitions
+    SMT.check >>= \case
+        Nothing -> pure ()
+        Just Sat -> pure ()
+        Just Unsat -> errorInconsistentDefinitions
+        Just Unknown -> do
+            SMT.localTimeOut quadrupleTimeOut $
+                SMT.check >>= \case
+                    Nothing -> pure ()
+                    Just Sat -> pure ()
+                    Just Unsat -> errorInconsistentDefinitions
+                    Just Unknown -> errorPossiblyInconsistentDefinitions
   where
+    quadrupleTimeOut :: SMT.TimeOut -> SMT.TimeOut
+    quadrupleTimeOut (SMT.TimeOut Unlimited) = SMT.TimeOut Unlimited
+    quadrupleTimeOut (SMT.TimeOut (Limit r)) = SMT.TimeOut (Limit (4 * r))
+
     declareRule ::
         SentenceAxiom (TermLike VariableName) ->
         m (Maybe ())
@@ -173,6 +189,8 @@ declareSMTLemmas tools lemmas = do
 
     ~errorInconsistentDefinitions =
         error "The definitions sent to the solver are inconsistent."
+    ~errorPossiblyInconsistentDefinitions =
+        error "The definitions sent to the solver may not be consistent (Z3 timed out)."
 
 translateUninterpreted ::
     ( Ord variable