z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
I tried to solve a Teacher Assignment Problem using the vZ extension. I have several constraints and a cost function that needs to be minimized. But the output is clearly...
smt2 file: https://gist.github.com/leonardoalt/ab12713eb249dadb86f7bb1441705e59 @agurfinkel we once talked about cex not working super well when using nonlinear arithmetic, but this didn't happen before (this happened now on a regression test). ```...
The below script is satisfiable; a bit hard to read but cvc4 finds a model successfully: ``` $ cvc4 --strings-exp c.smt2 sat (model (define-fun s0 () (Seq (Seq Int)) (seq.++...
Currently to use the Java API on Linux platform, the developer must explicitly compile and link the dynamic libraries. It would be much easier to integrate Z3 to an existing...
The following SMT queries get evaluated in less than a second in 4.8.7.0 but takes a long time in 4.8.8.0 and later. ``` (declare-const db_select_s_str_1 String) (assert (let ((a!1 (not...
Hi there! I see that z3 has support for pkg-config via CMake: https://github.com/Z3Prover/z3/blob/658a334ecf5a06553ad16d2104440e892b31c31c/z3.pc.cmake.in I noticed that there's a reference to pkg-config in the Make-based build system: https://github.com/Z3Prover/z3/blob/658a334ecf5a06553ad16d2104440e892b31c31c/scripts/mk_util.py#L45 ...but it doesn't...
I am having a problem when trying to use the Z3Str3 from z3-4.8.9-x64-ubuntu-16.04 notably if I substitute the com.microsoft.z3.jar to the one in z3-4.8.8-x64-ubuntu-16.04 I no longer have that issue....
Hello! I've noticed a very significant slow down past z3 v4.8.10, that I've bisected to originates without any doubt from the above mentioned commit. I have very long smt2 files...
I have this one case where Spacer returns `unknown` when I run all my regression tests together (heavy load), whereas it returns `unsat` if I run just the single test...
z3 version: 4.8.9 ~~The query is https://gist.github.com/leonardoalt/ae660a952383d3f6aff50dc0eee96164. The seg fault happens via the C++ API. I haven't managed yet to run the cli z3 because of https://github.com/Z3Prover/z3/issues/4689, so posting the...