Don't crash on unsatisfiable configurations. (#2765)

* Don't crash on unsatisfiable configurations.

See #2751.

* Added unit test for unsatisfiable patterns.

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: RaoulSchaffranek

kore/src/Kore/Exec.hs

@@ -258,7 +258,7 @@ exec
                         , (ExecDepth 0, Start initialConfig)
                         )
             let (depths, finalConfigs) = unzip finals
-            infoExecDepth (maximum depths)
+            infoExecDepth (maximum (ExecDepth 0 : depths))
             let finalConfigs' =
                     MultiOr.make $
                         catMaybes $

kore/test/Test/Kore/Exec.hs

@@ -1,6 +1,7 @@
 module Test.Kore.Exec (
     test_exec,
     test_execPriority,
+    test_execBottom,
     test_searchPriority,
     test_searchExceedingBreadthLimit,
     test_execGetExitCode,
@@ -194,6 +195,30 @@ test_exec = testCase "exec" $ actual >>= assertEqual "" expected
     inputPattern = applyToNoArgs mySort "b"
     expected = (ExitSuccess, applyToNoArgs mySort "d")
 
+test_execBottom :: TestTree
+test_execBottom = testCase "exec returns bottom on unsatisfiable input patterns." $
+    do
+        ((_, actual), _) <- result
+        assertEqual "" expected actual
+  where
+    expected = mkBottom mySort
+    result =
+        exec
+            Unlimited
+            Unlimited
+            verifiedModule
+            Any
+            inputPattern
+            & runTestLog runNoSMT
+    verifiedModule =
+        verifiedMyModule
+            Module
+                { moduleName = ModuleName "MY-MODULE"
+                , moduleSentences = []
+                , moduleAttributes = Attributes []
+                }
+    inputPattern = mkBottom mySort
+
 test_searchPriority :: [TestTree]
 test_searchPriority =
     [makeTestCase searchType | searchType <- [ONE, STAR, PLUS, FINAL]]