src/HOL/Tools/SMT/z3_interface.ML
changeset 47965 8ba6438557bc
parent 46497 89ccf66aa73d
child 49720 6279490e0438
     1.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed May 23 15:40:10 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed May 23 16:03:38 2012 +0200
     1.3 @@ -184,7 +184,8 @@
     1.4    end
     1.5  
     1.6  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
     1.7 -val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
     1.8 +val add = Thm.cterm_of @{theory} @{const plus (int)}
     1.9 +val int0 = Numeral.mk_cnumber @{ctyp int} 0
    1.10  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
    1.11  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
    1.12  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
    1.13 @@ -211,7 +212,7 @@
    1.14    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
    1.15    | _ =>
    1.16      (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
    1.17 -      (Sym ("+", _), SOME @{typ int}, [ct, cu]) => SOME (mk_add ct cu)
    1.18 +      (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
    1.19      | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
    1.20      | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
    1.21      | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu)