Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use CVC4 instead of CVC3 at CASC
authorblanchet
Mon, 22 Jun 2015 16:56:03 +0200
changeset 60543 ea2778854739
parent 60542 c5953e3a1e4f
child 60544 3daf5eacec05
use CVC4 instead of CVC3 at CASC
src/HOL/TPTP/atp_problem_import.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/TPTP/atp_problem_import.ML	Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Jun 22 16:56:03 2015 +0200
@@ -243,7 +243,7 @@
     (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
   ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
isabelle