z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/8f4ffc7caf19ba9c7b4c63935ef19cef215e847f incorrectly returns `unsat` with `(check-sat-using qsat)`. ``` $ z3 small.smt2 sat unsat $ cat small.smt2 (declare-const x (Array Bool Bool)) (declare-fun a ()...
I've been trying to cross-compiling z3 for arm32 on a x64 machine with arm-linux-gnu toolchain and clang/clang++, with the following environment settings: ``` export CC=clang-15 export CXX=clang++-15 export CFLAGS="-fno-inline -g...
Greetings, For this instance, an invalid bug occurred. We tried to make this instance as small as possible. We sincerely hope that our report will be helpful for the z3...
We are hacking formulas with a theory of regular languages. In two cases below first one reports unsat correctly, but second one hangs. It looks like combination of propositional language...
The following input: ``` (push) (declare-datatype Pair ((mkPair (fst Bool) (snd Bool)))) (assert (= (fst (mkPair true false)) (fst (mkPair false false)))) (check-sat) (pop) (push) (declare-datatype Pair ((mkPair (snd Bool)...
hi, trying to use z3-solver in a project but i'm unable to import the module properly. ``` [9:51:56 AM] ERROR [worker reload] [worker init] Directory import '/Users/uwes/src/mixed/z3_issue/nuxt-app/node_modules/.pnpm/[email protected]/node_modules/z3-solver/build/high-level' is not supported...
I tried executing the newest z3 release on my raspberry pi, but the executable seems to be built for x86_64 ## How to Reproduce the issue ```sh wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.0/z3-4.13.0-arm64-glibc-2.35.zip unzip...
I ran into a huge performance issue using datatypes, bitvectors, and shallow linear recursion (depth
Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/2682c2ef2b3f31f065cc54b83e91f6d42c60db2f debug build ``` $ cat small.smt2 (declare-fun b () (_ FloatingPoint 3 2)) (assert (exists ((a (_ FloatingPoint 3 2)) (a (_ FloatingPoint...