z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
Dear Z3 developers, I wanted to kindly suggest two improvements for your releases, especially for the Java bindings in your artifacts: - always include Java bindings for all platforms (Java...
The SMT2 input below exhibits brittle behavior in how quantifiers are instantiated or used. We frequently see this kind of brittleness through Dafny, but it's been difficult to construct a...
The example below does not seem to terminate. Removing either of the three quantified assertions makes z3 terminate, though it still takes several seconds (with some variation depending on which...
Hi! Z3 [version 4.13.1 - 64 bit] ubuntu:22.04 ``` cat test.smt2 (set-option :smt.string_solver z3str3) (set-logic QF_SLIA) (declare-fun s1 () String) (declare-fun s2 () String) (assert (str.in.re s2 (re.inter (re.* (re.union...
This issue/question is about the default approach that z3 takes to solve queries involving array and bitvector theory. The application we have is using these two theories to model binary...
``` 18:36 ➜ z3 --version Z3 version 4.13.0 - 64 bit ``` [mwe.smt.txt](https://github.com/user-attachments/files/16732114/mwe.smt.txt) contents of mwe.smt.txt ```smt (set-option :print-success true) (set-option :produce-models true) (declare-datatype cn_tuple_0 ((cn_tuple_0))) (declare-datatype cn_tuple_2 (par (a0...
Greetings, For this instance, cvc5 gives us "SAT" with a validated model. We tried to minimize the instance as small as possible. Truly hope that this instance will be helpful...
Greetings, For this instance, an invalid model bug occurred. We checked other issues on string theory(#6857, #6907). These instances do not trigger invalid model bugs anymore on the current commit...
After upgrading from Z3 version 4.13.2 to 4.14.1, I noticed a significant performance regression when using the OCaml bindings to invoke the Fixedpoint (CHC) solver (from 5 hours) To isolate...
