z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
``` [511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 Failed to validate 60 741: (= (o (a #186)) (o (a #668))) false (sat ... [512] % cat small.smt2 (declare-datatypes ((a 0))...
Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/6910a4e18c38e53afea2abe270ac9b2dec040c53 debug build ``` $ cat small.smt2 (declare-const x (Array Bool Int)) (assert (forall ((v (Array Bool Int))) (distinct 0 (select (store x (=...
``` [529] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 Failed to validate 76 147: (= (extract[31:31] (bv_wrap a)) (extract[31:31] (bv_wrap #80))) true (sat ... [530] % cat small.smt2 (declare-fun a () Float32)...
Hello, The latest release build of z3 (https://github.com/Z3Prover/z3/commit/479f8442009987726e3c03fe5618b250acca383a) hangs on this instance, while z3-4.8.1 produces results quickly. ``` $ cat small.smt2 (declare-fun r () String) (assert (> (str.indexof (str.substr r...
The following testcase from Symbiyosys (executed with `z3 -smt2 -in`) crashes on OpenBSD -current. ``` ; SMT-LIBv2 description generated by Yosys 0.32 (git sha1 fbab08acf14, c++ 13.0.0 -O2 -fPIC -Os)...
The `.dylib` distributed in the `pip` package of `z3` seems to have bad version info in it. Here is a comparison of the version distributed through homebrew vs pip. Notice...
I'm experimenting with adjusting a Z3-based tool to produce bitvector encodings of its problems rather than integer encodings. This is producing surprising performance regressions. The tool I'm working on is...
Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/cafe3acff1d4aedf2b08a4700574fcb41b4e4355 incorrectly gives `unsat` with `(check-sat-using qe)`. ``` $ cat small.smt2 (declare-fun a () Real) (assert (and (forall ((v Real)) (= (= a v)...
Hi, For this formula, ``` (set-logic NRA) (declare-fun a () Real) (declare-fun b () Real) (declare-fun c () Real) (declare-fun d () Real) (declare-fun e () Real) (declare-fun f ()...
``` [578] % z3release model_validate=true small.smt2 sat sat sat sat sat (error "line 16 column 10: an invalid model was generated") ( (define-fun a () Bool false) (define-fun s ()...
