z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
Hangs when using the builtin `z3.PartialOrder`: ```py from z3 import * T = DeclareSort("T") Less = PartialOrder(T, 0) Bot, x = Consts("Bot x", T) solver = Solver() solver.add(ForAll([x], Less(Bot, x)))...
Dear Z3 team, In recent experiments, we ran into some problems with the Python API when optimizing over boolean constraints. We generate a large number of constrained assignment problem over...
I would like to inquire your opinion on a feature idea that would IMHO make the use of Z3 significantly more flexible as well as open up new application areas....
``` [682] % z3 small.smt2 sat unsat [683] % [683] % cat small.smt2 (set-option :fp.spacer.gpdr true) (declare-fun a (Bool Bool Int Int Int Int Int Int Int) Bool) (assert (forall...
Running spacer or pdr on the SMT file below, I get the following output ``` sat (model (define-fun |g$unknown:5| ((x!0 Int) (x!1 Int)) Bool true) (define-fun |f$unknown:3| ((x!0 Int) (x!1...
For a func decl `d` of a floating-point numeral expression: - `Z3_get_decl_kind (ctx, d)` returns `Z3_OP_FPA_NUM`. - `Z3_get_decl_num_parameters (ctx, d)` returns 1. - `Z3_get_decl_parameter_kind (ctx, d, 0)` returns `Z3_PARAMETER_FUNC_DECL`. -...
Hello everyone, I am currently working with Z3 version 4.13.0 and think that z3 returns erroneously SAT for the following CHC-formula: ``` (set-logic HORN) (declare-fun inv1 (Int (Array Int Int)...
I would have expected that the following constraint is unsat (there is no strict superset of Bool). However, I do get a solution ``` ; when replacing Bool by Int...
Hi, we found this failure while upgrading F* projects, specifically HACL* to Z3 4.13.3. Some files were taking considerably longer times when compared to Z3 4.8.5 (>1 hour from just...
Hello. I've found out that asserting no multiplication overflow is very slow when the answer is unsat. The simplest example I was able to produce is as follows: ``` (declare-fun...
