z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
A new variation of #7121 has cropped up: ``` from z3 import * z3.set_param("model", True) z3.set_param("model.completion", True) z3.set_param("verbose", 10) ctx = z3.Context(model=True) slvr = z3.Solver(ctx=ctx) slvr.set("model", True) slvr.set("model.completion", True) S...
I have this relatively simple problem where Z3 in versions 4.8.5 and 4.13.0 (2 I tested) seems to hang indefinitely: ``` (declare-fun a () Int) (declare-fun b () Int) (declare-fun...
Commit: https://github.com/Z3Prover/z3/commit/0b3bbc297248849cb17c29e0fbaa23f61bb45716 OS: Ubuntu 22.04 ``` [523] % time z3-4.11.2 small.smt2 sat real 0m0.112s user 0m0.035s sys 0m0.009s [524] % timeout -s 9 10 z3release small.smt2 Killed [525] % cat...
I'm using the Z3 API on OCaml (z3 opam version `4.12.5`) and I found a strange behavior. When I try to get a function declaration like this, ```ocaml Z3.Expr.get_func_decl expr...
0b3bbc297248849cb17c29e0fbaa23f61bb45716 ``` $z3release model_validate=true bug.smt2 sat (error "line 7 column 12: an invalid model was generated") $cat bug.smt2 ( declare-const a0 (_ FloatingPoint 11 53) ) ( declare-const a1 (_...
```py from z3 import * Bool = BoolSort() S = FiniteDomainSort("S", 2) R = Function("R", S, S, Bool) TC_R = TransitiveClosure(R) x,y = Consts("x y", S) s = Solver() s.add(ForAll([x,...
I am trying to work with sequences (modeling SQL conditions, and need it to work with IN clauses of the form "US" in ImportCountries to see if two conditions can...
Getting unsound model with z3 from binary distribution [z3-4.12.5-x64-glibc-2.31.zip](https://github.com/Z3Prover/z3/releases/tag/z3-4.12.5) ``` $ z3 --version Z3 version 4.12.5 - 64 bit ``` ``` $ z3 -smt2 model.compact=false min.smt2.txt > model ``` Files:...
I have a non-incremental smtlib problem over QFBV + QFIDL ([smtlib.txt](https://github.com/Z3Prover/z3/files/14295610/smtlib.txt)) Z3 solves this in around 3 seconds (UNSAT). If I add a single `(push)` statement directly before `(check-sat)`, the...
Hi, z3 https://github.com/Z3Prover/z3/commit/a2fa4ff1bcefaf6499a200185c1c5500bcb20a13 gives `unknown` for the following simple instance, while z3-4.8.10 can yield `unsat`. ``` $ cat small.smt2 (declare-const x8 Bool) (declare-const x Int) (assert (forall ((e Real)) (=...
