Add support for CVC4 1.8 to Sledgehammer
authordesharna
Fri, 13 Nov 2020 09:47:59 +0100
changeset 72667 b83988b436dc
parent 72593 914f1f98839c
child 72668 b1388cfb64bb
Add support for CVC4 1.8 to Sledgehammer
src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Nov 12 17:42:15 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Nov 13 09:47:59 2020 +0100
@@ -77,10 +77,9 @@
 
 local
   fun cvc4_options ctxt = [
-    "--no-statistics",
+    "--no-stats",
     "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--lang=smt2",
-    "--continued-execution",
     "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
 
   fun select_class ctxt =