# HG changeset patch
# User blanchet
# Date 1434984963 -7200
# Node ID ea2778854739256ee9857341854d1791dad22ce8
# Parent  c5953e3a1e4f17e2f78063edf8a37b11fcaa3745
use CVC4 instead of CVC3 at CASC

diff -r c5953e3a1e4f -r ea2778854739 src/HOL/TPTP/atp_problem_import.ML
--- 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)