z3 Questions
2
I am running into the following error when using a python script (oyente) that uses Z3 (which I've built in the Visual Studio command prompt):
File "C:\Python27\Lib\site-packages\oyente\z3\z3core....
1
Solved
It was suggested in this Z3 issue comment that option rlimit is to be preferred over timeout:
Combining timeouts with a search algorithm makes everything
non-deterministic, so now you don't eve...
Mussman asked 2/8, 2017 at 9:39
1
Is there an incremental SMT solver or an API for some incremental SMT solver where I can add constraints incrementally, where I can uniquely identify each constraint by some label/name?
The reaso...
Monogenic asked 4/6, 2017 at 16:31
1
I am using the Python bindings for the Z3 theorem prover (Z3Py). I have N boolean variables, x1,..,xN. I want to express the constraint that exactly K out of N of them should be true. How can I do ...
2
Solved
I am working on a program in Python in which a small part involves optimizing a system of equations / inequalities. Ideally, I would have wanted to do as can be done in Modelica, write out the equa...
1
Solved
How to convert a simple while loop(c- code) to smt2 language or z3?
For ex :
int x,a;
while(x > 10 && x < 100){
a = x + a;
x++;
}
1
Solved
I have a question regarding how Z3 incrementally solves problems. After reading through some answers here, I found the following:
There are two ways to use Z3 for incremental solving: one is push...
2
Z3 currently supports the DIMACS format for input. Is there any way to output the DIMACS format for the problem before solution? I mean converting the problem to a system CNFs and output it in a DI...
Emmettemmey asked 24/10, 2012 at 22:56
2
I am trying to perform some symbolic calculation on matrices (with symbols as an entries of matrices), and after that I will have a number of possible solution. My goal is to select solutions/ solu...
1
I understand that nonlinear integer arithmetic is basically Hilbert's tenth problem and is proven to be undecidable. However the Z3 solver is able to provide a complete solution for nonlinear real ...
2
Solved
Is there a complete listing of all theories/logics that z3 supports? I have consulted this SMTLIB Tutorial which provides a number of logics, but I do not believe that the list is exhaustive. The z...
1
Solved
Let say that I have some formulas that can be sat but I want to get the smaller (or larger) possible value so sat that formula.
Is there a way to tell the SMT solver to give that kind of small so...
1
Solved
I am having troubles proving the following law with LiquidHaskell:
It is known as (one of) DeMorgan's law, and simply states that the negation of oring two values must be the same as anding the ...
Jacksmelt asked 23/4, 2016 at 16:38
1
Solved
I'm trying to represent temporal constraints in SMT-LIB in order to check their satisfiability. I'm looking for feedback on the direction I'm taking. I'm relatively new to SMT-LIB and I'll highly a...
2
Solved
Browsing Z3 source code, I came across a bunch of files referring to QF_FPA, which seems to stand for quantifier-free, floating-point-arithmetic. However, I don't seem to be able to locate any docu...
Sultry asked 3/3, 2013 at 0:46
1
Solved
I have a simple example in nonlinear integer arithmetic, namely a search for Pythagorean triples. Based on what I read in related questions (see below), I'd expect Z3 to find a solution to this pro...
0
Sorry that this question is subjective, but given that the Stack Overflow has the largest Z3 user base, I want to give it a try.
I have a big constraint satisfaction problem that consists of...
2
Solved
I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values:
class Test {
//@ requires b > 0;
void a(double b) {
}
void b() {
a(2.4);
}...
2
Solved
I'm using SBV (with Z3 backend) in Haskell to create some theory provers. I want to check if forall x and y with given constrains (like x + y = y + x, where + is a "plus operator", not addition) so...
1
Solved
Let's say I have a z3 solver with a certain number of asserted constraints that are satisfiable. Let S be a set of constraints, I would like to verify for every constraint in S whether the formula ...
Ptolemaic asked 14/6, 2015 at 11:4
1
Solved
I'm working on a Python project, where I'm currently trying to speed things up in some horrible ways: I set up my Z3 solvers, then I fork the process, and have Z3 perform the solve in the child pro...
7
Solved
I noticed some strange behavior with Z3 4.3.1 when working with .smt2 files.
If I do (assert (= 0 0.5)) it will be satisfiable. However, if I switch the order and do (assert (= 0.5 0)) it's not s...
Bonnie asked 16/7, 2014 at 20:46
2
Solved
In Z3, the following is clearly evaluated to a maximum of 2, with the model x=true and y=true.
(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert(= z false))
(maximize(
...
1
Solved
I'm trying to influence the randomness of results for model values generated by Z3. As far as I understand, the options for this are very limited: in case of linear arithmetic, the simplex solver d...
1
Solved
A very similar questions were asked on SO already, but I couldn't find answer to the following problem.
A linear maximization problem can be easily stated using for-all quantifier:
obj = f(x) AND...
Fusspot asked 12/6, 2014 at 11:57
© 2022 - 2024 — McMap. All rights reserved.