I would like to model fixed-size memory buffers and their access operations in Z3. The size of the buffers can be anywhere from a couple of bytes to hundreds of bytes. The standard way employed by ...

I met the following error while compiling z3. It seems to be an error for ld. I wonder what I can do to make it compile. It is a problem from the opt branch in git. I am on iMac with OS X 10.9.2 (1...

Suppose I have 2 arrays in a formula whose satisfiability I want to check using z3. If z3 returns sat, I want to read in the first array in the z3 model and pretty print it as a key, value pair and...

I have been trying to solve a small problem which includes absolute value of some terms. In z3 there is no support for abs() function. In python there is, but I eventually i have to pass it to z3py...

I am using the Java-API of Z3 Version 4.3.2 64-bit on Windows 7 as well as Java 7 64-bit, but I don't think Java is a necessity to answer this question. Right now I am using the following Java cod...

Today I wanted too look into options on SAT solving in haskell. First I tought about writing my own interface to the picosat solver. Then I found out there is the SBV library. It's interfaces to Z...

Has anyone tried proving Z3 with Z3 itself? Is it even possible, to prove that Z3 is correct, using Z3? More theoretical, is it possible to prove that tool X is correct, using X itself?

I've read the posts about nonlinear arithmetic and uninterpreted functions. I'm still very new to SMT world, so apologies if I'm not using the right vocabulary or this is a bad question. For the ...

I get confused about the following two declarations. For me, they describe the same thing: an integer variable x. (declare-const x Int) (declare-fun x () Int) Is there any context that make the...

In a previous post some problems involving operational amplifiers were solved using Z3Py online. But now that Z3Py online is out of service I am trying to solve such problems using Z3 SMT-LIB onlin...

I tried the following code in http://rise4fun.com/z3/tutorial (declare-const a Int) (assert (> a 100)) (check-sat) (get-model) the result is always a=101. I need some randomness in the answer...

Any more or less practical programming language and compiler have to deal with constraints. The most common constraint is types. Usually type derivation and unification is done by a straightforward...

I obtained several statistics from runs of Z3. I need to understand what these mean. I am rather rusty and non up to date for the recent developments of sat and SMT solving, for this reason I tried...

I am using Z3's python api to do some kind of incremental solving. I push constraints to the solver iteratively while checking for unsatisfiability at each step using solver.push() command. I want ...

I am using Z3 to extract the unsat-core of an unsatisfiable formula. I am using Z3@Rise interface (web based) to write the following code, (set-logic QF_LIA) (set-option :produce-unsat-cores true)...

I understand that Z3 has some supports for nonlinear arith but wondering to what extends ? Is it possible to specify what classes of nonlinear arithmetics are supported and are not (or likely to gi...

Say I have t1<x and x<t2 is it possible to hide variable x so that t1<t2 in Z3?

I get the following statistics in Z3. (:added-eqs 24529 :binary-propagations 43837 :bv-bit2core 7115 :bv-conflicts 156 :bv-diseqs 10395 :bv-dynamic-diseqs 10028 :bv->core-eq 10401 :confl...

Suppose that a is an integer of 8-bit of value 254. If a is a signed integer, it is actually considered -2. In contrary, if a is unsigned, it remains 254. I am trying to model this signed/unsigned...

For the below code, I have observed very fast results that seem to be caused/affected by three unusual aspects: When using (set-option :produce-proof true), the final UNSAT is very fast. Without ...

Over the years I keep track of solving technology - and I maintain a blog post about applying them to a specific puzzle - the "crossing ladders". To get to the point, I accidentally found out abo...

I'm trying to define a theory of sets (union, intersection etc.) for Z3 using the SMTLIB interface. Unfortunately, my current definition hangs z3 for a trivial query, so I guess I'm missing some ...

We know that, we can prove validity of a theorem by saying : let Demorgan(x, y) = formula1(x,y) iff formula2(x,y) assert ( forall (x,y) . Demorgan(x,y) ) Alternatively we can eliminate the fora...

The .net API has the following constructor for a Context: Context (Dictionary< string, string > settings) how to get a list of all the possible settings? Specifically, I am interested in ...

Find the value of R in the following circuit This problem is solved using the following code: R, V1, V2, Vo = Reals('R V1 V2 Vo') I1 = V1/(R -50) I2 = V2/(R + 10) g = - R*(I1 + I2) print g equa...