# HG changeset patch
# User boehmes
# Date 1253524521 -7200
# Node ID 8ed38c7bd21a66291640df1032f8dbaa8056fbbd
# Parent  35094c8fd8bff6a595644f624fafdd8475621810
corrected remote SMT solver invocation

diff -r 35094c8fd8bf -r 8ed38c7bd21a src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Mon Sep 21 08:45:31 2009 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Mon Sep 21 11:15:21 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])
 
 
diff -r 35094c8fd8bf -r 8ed38c7bd21a src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 08:45:31 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 11:15:21 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
diff -r 35094c8fd8bf -r 8ed38c7bd21a src/HOL/SMT/lib/scripts/remote_smt.pl
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl	Mon Sep 21 08:45:31 2009 +0200
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl	Mon Sep 21 11:15:21 2009 +0200
@@ -1,4 +1,3 @@
-#!/usr/bin/env perl -w
 #
 # Script to invoke remote SMT solvers.
 # Author: Sascha Boehme, TU Muenchen