# HG changeset patch
# User blanchet
# Date 1394713093 -3600
# Node ID 2cd8fcb4804d4c6d1d47dbb286233d8ca891291b
# Parent  fb160b829a8855e79eb2c7ee1ee19eb3997513f3
slacker error code policy for Z3

diff -r fb160b829a88 -r 2cd8fcb4804d src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -82,10 +82,12 @@
             File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
             I output))
 
+(* Z3 returns 1 if "get-model" or "get-model" fails *)
+val normal_return_codes = [0, 1]
+
 fun run_solver ctxt name mk_cmd input =
   let
-    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
-      (map Pretty.str ls))
+    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag (map Pretty.str ls))
 
     val _ = SMT2_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
 
@@ -96,7 +98,7 @@
     val output = fst (take_suffix (equal "") res)
     val _ = SMT2_Config.trace_msg ctxt (pretty "Result:") output
 
-    val _ = return_code <> 0 andalso
+    val _ = member (op =) normal_return_codes return_code orelse
       raise SMT2_Failure.SMT (SMT2_Failure.Abnormal_Termination return_code)
   in output end