z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
With Z3 4.8.12. The following python code reproduces the issue: ```python from z3 import * a = Re('a') b = Re('b') r1 = Concat(a, Star(Concat(b, a))) # a(ba)* r2 =...
Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/e423fabf6a8808c36d906cdd62dda9c90773992d ``` $ cat small.smt2 (declare-fun var810 () String) (assert (and (forall ((va String)) (or (= "B" var810) (not (str.in_re va (re.union (str.to_re "z") (str.to_re...
This is a simplified version of a problem reported in https://github.com/Z3Prover/z3/issues/4889. This input: ``` ...$ cat case_tactic.smt2 (declare-fun x () (_ FloatingPoint 11 53)) (declare-fun rm () RoundingMode) (assert (=...
I am trying to solve some geometric problem. While it looks impregnable for Z3 I am trying to shrink the goal in order to understand the limitations. To my surprise...
Hi, I am facing a weird result when using Z3. Consider these two benchmarks written in SMTLIB: ``` (declare-fun a () (Array (_ BitVec 32) (_ BitVec 32))) (declare-fun b...
Hi, for the following formula z3 incorrectly reports `sat` instead of `unsat`. ``` $ cat test.smt2 (declare-fun s () String) (declare-fun r () String) (assert (and (= "\u{2f}" (str.substr s...
We find some performance regression problems when using the instruction "z3 smt.string_solver=z3str3". The older version(say, z3-4.6.0) runs so fast, but the latest version is slow. **case1:** ``` (set-logic QF_S) (declare-fun...
``` (set-option :random-seed 42) (set-option :produce-models true) ; (set-info :status sat) (declare-fun tmp_reglan0 () (RegEx String)) (assert (let ((?x1276 (re.* re.allchar))) (let ((?x1279 (re.* tmp_reglan0))) (= ?x1279 ?x1276)))) (check-sat) (get-value...
Hi, For this case, Z3 gives an incorrect answer: ``` [1152] % z3-4.8.5 small.smt2 unsat sat [1153] % z3-4.8.6 small.smt2 unsat sat [1154] % z3-4.8.7 small.smt2 unsat sat [1155] %...
On the following problem: ```smt2 (set-logic HORN) (declare-fun inc (Int Int Int) Bool) (assert (forall ((x Int) (n Int)) (inc (+ n 1) x n))) (declare-fun inc2 (Int) Bool) (assert...
