--- a/src/HOL/SMT/Examples/SMT_Examples.thy Mon Sep 21 10:58:25 2009 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Mon Sep 21 11:15:55 2009 +0200
@@ -9,7 +9,7 @@
begin
declare [[smt_solver=z3, z3_proofs=false]]
-declare [[smt_trace=true]] (*FIXME*)
+declare [[smt_trace=false]]
section {* Propositional and first-order logic *}
@@ -163,6 +163,7 @@
(eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
eval_dioph ks (map (\<lambda>x. x div 2) xs) =
(l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
+ using [[smt_solver=z3]]
by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
--- a/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 10:58:25 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 11:15:55 2009 +0200
@@ -121,7 +121,7 @@
fun cmd f1 f2 =
if path <> ""
then map qq (path :: args) @ [qf f1, ">", qf f2]
- else map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
+ else "perl -w" :: map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end
end
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl Mon Sep 21 10:58:25 2009 +0200
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl Mon Sep 21 11:15:55 2009 +0200
@@ -1,4 +1,3 @@
-#!/usr/bin/env perl -w
#
# Script to invoke remote SMT solvers.
# Author: Sascha Boehme, TU Muenchen