capture error messages (of SMT solvers)
authorboehmes
Tue, 02 Feb 2010 23:38:41 +0100
changeset 34997 7cc8726aa8a7
parent 34996 51c93ab92c3e
child 34998 5e492a862b34
child 35505 4d202d722eb2
capture error messages (of SMT solvers)
src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 02 19:30:08 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 02 23:38:41 2010 +0100
@@ -159,7 +159,7 @@
     system_out (space_implode " " ("perl -w" ::
       File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
       map File.shell_quote (solver @ args) @
-      map File.shell_path [problem_path, proof_path]))
+      map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
   end
 
 in