z3

z3 copied to clipboard

(z3str3) Soundness bug on QF_S formula with re.comp str.to_re

2

Hi, For this case, Z3 gives an incorrect answer: ``` [573] % z3 smt.string_solver=z3str3 small.smt2 sat [574] % z3 small.smt2 unsat [575] % [575] % cat small.smt2 (set-logic QF_S) (assert...

muchang

(z3str3, smt.phase_selection=1) Soundness bug on QF_S formula with str.at and str.substr

2

Hi, For this case, Z3 gives an incorrect answer: ``` [572] % z3 small.smt2 unsat [573] % z3 smt.arith.solver=2 small.smt2 unsat [574] % z3 smt.arith.solver=2 smt.string_solver=z3str3 small.smt2 unsat [575] %...

muchang

A QF_S test case make z3 unable to return results

1

For this test case, I can get the result "unsat" quickly by using cvc4, but z3 can't get the result for a long time. ``` (set-logic QF_S) (declare-fun var0 ()...

drogonFan

``` (set-logic QF_S) (declare-fun var3 () Int) (declare-fun var0 () String) (declare-fun var2 () String) (assert (> (str.indexof "+]YAPKJ8b8" var2 var3) (str.to.int var0))) (check-sat) ```  This test case triggers...

drogonFan

Massive space leak with simple sequence benchmark

3

The following benchmark is actually rather simple, in the sense that a simple substitution of variables should find the `sat` model relatively quickly. Indeed, up until Nov 29th, z3 quickly...

LeventErkok

Memory leak in Z3 Context using .NET API

11

When instance of `Context` is created and disposed memory leak is observed. **Z3 Version:** 4.8.10 (also reproducible with previous versions) ### **Steps to reproduce (C#):** ``` // Check allocated memory...

GennadyGS

Nightly releases don't seem to match what's in the master

5

@NikolajBjorner It appears something is off with the nightly releases. If I go to: https://github.com/Z3Prover/z3/releases/tag/Nightly And get the latest "Source-code" as listed in the `Assets` section and look at the...

LeventErkok

Unexpected performance regression on a simple-looking query

38

Z3 4.8.8 solves this query instantly (as well as all previous releases as far as I can remember), while the new Z3 4.8.9 times out: [pero.zip](https://github.com/Z3Prover/z3/files/5258014/pero.zip) This is pretty unexpected...

zvonimir

Disable modules to reduce binary size

5

Sorry if this is more a question than an issue to be reported. We are trying to integrate z3 into a compiler ( http://github.com/ethereum/solidity/ ) but are currently a little...

chriseth

Reasoning with Regex

18

The following smt input ``` (set-info :smt-lib-version 2.5) (assert (forall ((x String)) (= (str.in.re x (re.++ (str.to.re "a") (re.* (str.to.re "a")))) (str.in.re x (re.+ (str.to.re "a"))) ) ) ) (check-sat)...

pjljvandelaar