mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add arguments to optimize_check fix #1866

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-14 20:44:46 -07:00
parent 09e40f6e23
commit b1ab473035
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/ml/z3.ml
View file

@ -1952,7 +1952,7 @@ struct
let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e) let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e)
let check (x:optimize) = let check (x:optimize) =
let r = lbool_of_int (Z3native.optimize_check (gc x) x 0 []) 0 in let r = lbool_of_int (Z3native.optimize_check (gc x) x 0 []) in
match r with match r with
| L_TRUE -> Solver.SATISFIABLE | L_TRUE -> Solver.SATISFIABLE
| L_FALSE -> Solver.UNSATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE