merged

--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 17:04:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 18:04:04 2010 +0100
@@ -106,11 +106,6 @@
   map File.shell_quote (solver @ args) @
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
-fun check_return_code {output, redirected_output, return_code} =
-  if return_code <> 0 then
-    raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
-  else (redirected_output, output)
-
 fun run ctxt cmd args input =
   (case C.certificates_of ctxt of
     NONE => Cache_IO.run (make_cmd (choose cmd) args) input
@@ -124,7 +119,7 @@
       | (SOME output, _) =>
          (tracing ("Using cached certificate from " ^
             File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
-          output))) |> check_return_code
+          output)))
 
 in
 
@@ -135,11 +130,15 @@
 
     val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
 
-    val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
+    val {redirected_output=res, output=err, return_code} =
+      C.with_timeout ctxt (run ctxt cmd args) input
     val _ = C.trace_msg ctxt (pretty "Solver:") err
 
     val ls = rev (snd (chop_while (equal "") (rev res)))
     val _ = C.trace_msg ctxt (pretty "Result:") ls
+
+    val _ = null ls andalso return_code <> 0 andalso
+      raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
   in ls end
 
 end

--- a/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 15 17:04:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 15 18:04:04 2010 +0100
@@ -114,18 +114,30 @@
   let
     fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
 
-    val ints =
-      find_first (match [@{term int}]) vs
-      |> Option.map (fn (_, cases) =>
-           let val (cs, (_, e)) = split_last cases
-           in (e, map (apfst hd) cs) end)
-    fun nat_of (v as Value _) = 
-          (case ints of
-            NONE => v
-          | SOME (e, tab) => the_default e (AList.lookup (op =) tab v))
-      | nat_of e = e
+    val (default_int, ints) =
+      (case find_first (match [@{term int}]) vs of
+        NONE => (NONE, [])
+      | SOME (_, cases) =>
+          let val (cs, (_, e)) = split_last cases
+          in (SOME e, map (apfst hd) cs) end)
+
+    fun nat_of @{typ nat} (v as Value _) =
+          AList.lookup (op =) ints v |> the_default (the_default v default_int)
+      | nat_of _ e = e
+
+    fun subst_nat T k ([], e) =
+          let fun app f i = if i <= 0 then I else app f (i-1) o f
+          in ([], nat_of (app Term.range_type k T) e) end
+      | subst_nat T k (arg :: args, e) =
+          subst_nat (Term.range_type T) (k-1) (args, e)
+          |> apfst (cons (nat_of (Term.domain_type T) arg))
+
+    fun subst_nats (v as ((n, k), cases)) =
+      (case Symtab.lookup terms n of
+        NONE => v
+      | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
   in
-    map (subst nat_of) vs
+    map subst_nats vs
     |> filter_out (match [@{term int}, @{term nat}])
   end