# HG changeset patch
# User desharna
# Date 1605257279 -3600
# Node ID b83988b436dc113e9da2783515d16ffc4c287782
# Parent  914f1f98839ce73812119ef097b1c2c531e95e28
Add support for CVC4 1.8 to Sledgehammer

diff -r 914f1f98839c -r b83988b436dc 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 =