Hi all! Does anyone here have experience using the Z3 OCaml API? (I’m using version 4.8.14.0 the latest one).

I have run into a rather mind-bending situation where Z3’s decision changes when I invoke it through the API vs submit a query via the command line binary.

Here is the SMTLib2 query that I’m submitting to z3:

(declare-datatypes ((list 0)) (((nil) (cons (head Int) (tail list)))))
(declare-fun repeat (Int Int) list)
(declare-fun vl () Int)
(declare-fun len () Int)
(assert (forall ((len Int) (vl Int))
(let ((a!1 (= (repeat len vl) (cons vl (repeat (- len 1) vl)))))
(ite (<= len 0) (= (repeat len vl) nil) a!1))))
(assert (> len 0))
(assert (let ((a!1 (= (repeat len last) (cons last (repeat (- len 1) last)))))
(not a!1)))
(check-sat)

The query is mostly useless - I’ve minimalised it for ease of reading - but when submit to Z3, as one might expect, the solver outputs UNSAT.

Now, confusingly, when I try to submit the exact[1] query through the OCaml API, the solver outputs SAT[2].

I assume this is happening because when running from the command line some solver parameters are set that are not set when running from the API, but I have no idea how to go about fixing this.

Has anyone run into this problem? Is there a mistake with my code?

How did you end up making Z3 behave the same between the API and CLI?

This feels like a bug, so I’ve made an issue on the Z3 git repository, but wanted to check here if someone else has encountered this as well to avoid wasting the maintainer’s time.

[1] I know it is exact, because the SMTLib2 query above was actually generated directly by calling the Z3.Solver.to_string function provided by the API, see code below.

[2] My OCaml code:

let ctx = Z3.mk_context []
let sym s = Z3.Symbol.mk_string ctx s
let declare var ty = Z3.Expr.mk_const_s ctx var ty
let int = Z3.Arithmetic.Integer.mk_sort ctx
let list = Z3.Z3List.mk_sort ctx (sym "list") int
let cons =
let cons = Z3.Z3List.get_cons_decl list in
fun hd tl -> Z3.Expr.mk_app ctx cons [hd;tl]
let nil = Z3.Z3List.nil list
let repeat =
let repeat = Z3.FuncDecl.mk_func_decl ctx (sym "repeat") [int; int] list in
fun len vl -> Z3.Expr.mk_app ctx repeat [len;vl]
let (-) l r = Z3.Arithmetic.mk_sub ctx [l;r]
let (=) l r = Z3.Boolean.mk_eq ctx l r
let not cond = Z3.Boolean.mk_not ctx cond
let (<=) l r = Z3.Arithmetic.mk_le ctx l r
let (>) l r = Z3.Arithmetic.mk_gt ctx l r
let ite cond l r = Z3.Boolean.mk_ite ctx cond l r
let i v = Z3.Arithmetic.Integer.mk_numeral_i ctx v
let repeat_spec =
let len = Z3.Expr.mk_const_s ctx "len" int in
let vl = Z3.Expr.mk_const_s ctx "vl" int in
Z3.Quantifier.mk_forall ctx [int; int] [sym "len"; sym "vl"]
(ite (len <= i 0)
((repeat len vl) = nil)
(repeat len vl = cons vl (repeat (len - i 1) vl))
) None [] [] None None
|> Z3.Quantifier.expr_of_quantifier
let do_test () =
let solver = Z3.Solver.mk_solver ctx None in
Z3.Solver.add solver [repeat_spec];
let len = declare "len" int in
let last = declare "last" int in
Z3.Solver.add solver [len > i 0];
print_endline @@ (Z3.Solver.to_string solver);
let goal = (not (repeat len last = (cons last (repeat (len - i 1) last)))) in
Printf.printf "(assert %s)\n(check-sat)\n" @@ Z3.Expr.to_string goal;
match Z3.Solver.check solver [goal] with
| Z3.Solver.UNSATISFIABLE -> print_endline "unsat"
| Z3.Solver.UNKNOWN -> print_endline "unknown"
| Z3.Solver.SATISFIABLE -> print_endline "sat"

When running the above code, my program outputs sat.

The smtlib format is not detailed enough to exactly recreate the internal state that a sequence of API (OCaml or whatever) calls produces. In particular the order in which terms are constructed influences their internal identifiers, and various heuristics are sensitive to those ids. So for instance which order case splits are tried in can be affected by the order in which terms are constructed. This sort of thing can reasonably affect runtime, and sometimes can (at least several versions ago) cause an unknown versus definite answer. But I think that it is a bug for it to be able to change SAT vs UNSAT. There might be cases where the smtlib semantics differs from the Z3 semantics enough to be significant, but this example looks benign.

I received a response on the git repo issue tracker and the fault was on my end.

Just for propriety and for the benefit of future readers who run into a similar problem, the issue was due to the use of Z3.Quantifier.mk_forall which expects that the variables in its body have been bound by Z3.Quantifier.mk_bound, while I was passing in symbols declared as const.

Given this use case, the correct way to encode the quantifier is Z3.Quantifier.mk_forall_const.