Reset SMT solver (#2096)

Author: andreiburdusa

kore/app/exec/Main.hs

@@ -851,8 +851,12 @@ execute options mainModule worker =
             None -> withoutSMT
   where
     withZ3 =
-        SMT.runSMT config $ do
-            give (MetadataTools.build mainModule) (declareSMTLemmas mainModule)
+        SMT.runSMT
+            config
+            ( give
+                (MetadataTools.build mainModule)
+                (declareSMTLemmas mainModule)
+            )
             worker
     withoutSMT = SMT.runNoSMT worker
     KoreExecOptions { smtTimeOut, smtPrelude, smtSolver } = options

kore/app/repl/Main.hs

@@ -253,10 +253,13 @@ mainWithOptions
                             \ when running the repl in run-script mode."
                         exitFailure
 
-                SMT.runSMT smtConfig $ do
-                    give (MetadataTools.build indexedModule)
-                        $ declareSMTLemmas indexedModule
-                    proveWithRepl
+                SMT.runSMT
+                    smtConfig
+                    ( give
+                        (MetadataTools.build indexedModule)
+                        (declareSMTLemmas indexedModule)
+                    )
+                    $ proveWithRepl
                         indexedModule
                         specDefIndexedModule
                         Nothing

kore/bench/exec/Main.hs

@@ -229,31 +229,3 @@ tests:
       - template-haskell >=2.14
       - temporary >=1.3
     <<: *common-exe
-
-benchmarks:
-  kore-parser-benchmark:
-    main: Main.hs
-    other-modules:
-      - Paths
-    source-dirs:
-      - bench/parser
-      - test
-    dependencies:
-      - kore
-      - criterion >=1.5
-      - template-haskell >=2.14
-    <<: *common-exe
-
-  kore-exec-benchmark:
-    main: Main.hs
-    other-modules:
-      - Paths
-    source-dirs:
-      - bench/exec
-      - test
-    dependencies:
-      - kore
-      - criterion >=1.5
-      - template-haskell >=2.14
-      - temporary >=1.3
-    <<: *common-exe

kore/bench/parser/Main.hs

@@ -175,6 +175,7 @@ import Logic
     )
 import qualified Logic
 import qualified Pretty
+import qualified SMT
 
 {- | The final nodes of an execution graph which were not proven.
 
@@ -527,8 +528,10 @@ transitionRule claims axiomGroups = transitionRuleWorker
 
     transitionRuleWorker Begin Proven = empty
     transitionRuleWorker Begin (GoalStuck _) = empty
-    transitionRuleWorker Begin (GoalRewritten goal) = pure (Goal goal)
-    transitionRuleWorker Begin proofState = pure proofState
+    transitionRuleWorker Begin (GoalRewritten goal) =
+        SMT.reinit >> pure (Goal goal)
+    transitionRuleWorker Begin proofState =
+        SMT.reinit >> pure proofState
 
     transitionRuleWorker Simplify proofState
       | Just goal <- retractSimplifiable proofState =