z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
Hi, z3 https://github.com/Z3Prover/z3/commit/a8da0a685184ffbe89292ac1f325c8ae32c68303 produces an invalid model for the instance I've attached. Unfortunately, I'm unable to provide a reduced test case as the delta debugging tools cannot reduce the instance....
Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/dd906893394344d7a68ea38f57ec83195744f81b ``` $ z3 small.smt2 unsat ASSERTION VIOLATION File: ../src/nlsat/nlsat_interval_set.cpp Line: 94 !is_zero(s) || curr.m_upper_open || next.m_lower_open (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB s...
I `npm install`ed the z3-solver package, and then imported it, hoping that it would work in the browser. Since I didn't want to deal with the differences between CommonJS and...
Hi, I attempted to run solver.check() using the Java API and (check-sat) in commandline-tool to compare the runtimes. I understand that the Java API may be slightly slower than commandline-tool,...
Hello everyone! I recently added the 'z3-solver' npm package to my Angular app, updated all the necessary dependencies, and conducted some tests with numeric values. Working with numeric values went...
In the following code against 4.12.2, if `parallel.enable` is set to True, Python crashes the the below stack trace. When set to False, the code does not crash. My requirements.txt...
Greetings, For this instance, an invalid bug occurred. We tried to make this instance as small as possible. We sincerely hope that our report would be helpful for the z3...
Commit: https://github.com/Z3Prover/z3/commit/278d5a348217951b5f52729fd0ca6110eddd2426 OS: Ubuntu 22.04 ``` [513] % z3release model_validate=true small.smt2 sat (error "line 5 column 10: an invalid model was generated") ( (define-fun b () String "1003") (define-fun a...
Commit: https://github.com/Z3Prover/z3/commit/e8929041b840ce7d04df8ce101d408042d2a4384 OS: Ubuntu 22.04 ``` [548] % z3debug small.smt2 ASSERTION VIOLATION File: ../src/math/polynomial/algebraic_numbers.cpp Line: 2462 !nested_call (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [549] % cat small.smt2 (declare-fun...
Z3 version 4.8.8.0 Python version 3.8.2 ``` $ pip3 show z3-solver Name: z3-solver Version: 4.8.8.0 Summary: an efficient SMT solver library Home-page: https://github.com/Z3Prover/z3 Author: The Z3 Theorem Prover Project Author-email:...
