z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
For [this example](https://gist.github.com/blishko/33f40fe69d4ac3c8b75aac69da9c9960) I am getting an error when running Z3 (both Z3 4.8.9 and current master 620204bbb) with the option `fp.xform.inline_eager=false`. The error reported is `(error "line 289 column...
Hello Z3 team, while maintaining a SPARK codebase from a few years ago (red black trees) I noticed a notable regression in the provability. In fact, most checks in the...
Given the solver: (set-info :status unknown) (declare-fun full_string () String) (declare-fun string_contents () String) (declare-fun length_constraint () Int) (assert (= (str.indexof full_string "\x00" 0) (- (str.len full_string) 1))) (assert (let...
Hi, Regarding issue #1614, we ran the following query with and without **smt.string_solver=z3str3**. The speedup **in favor of** smt.string_solver=z3str3 was the biggest we've seen so far (**100x**) We wanted to...
Hi, I have the following simple unsat query for which **z3 returns immediately with a correct answer**. When I try it with **smt.string_solver=z3str3**, it hangs (for at least 10 mins...
Tested on HEAD (81ec5bae9500756bd7ea28a1da28afcdb0ca848f). The following [file](https://github.com/Z3Prover/z3/files/1507923/str5.txt) produces either sat or unsat depending on whether z3str3 was used. Expected is sat.
Hi, For this formula: ``` (declare-fun a () String) (declare-fun b () Int) (assert (distinct (str.replace "A" (int.to.str b) a) (str.replace "" (int.to.str b) a))) (assert (= (str.replace a (str.at...
Hi, For this formula: ``` (declare-fun x () String) (declare-fun y () String) (assert (distinct (str.replace (str.replace x y x) x y) x)) (check-sat) (get-model) ``` Z3 smt.string_solver=z3str3 gives an...
Hello, this file: [tmp8.txt](https://github.com/Z3Prover/z3/files/1503935/tmp8.txt) is very hard for the solver and it seems to run indefinitely. Is this perhaps a bug? A human can immediately find a counterexample for such...
Hi, For this formula, Z3 throws out an assertion violation: ``` [582] % z3release smt.string_solver=z3str3 small.smt2 ASSERTION VIOLATION File: ../src/smt/theory_str_mc.cpp Line: 1162 NOT IMPLEMENTED YET! Z3 4.8.9.0 Please file an...