FAQ Database Discussion Community

Difficulty in Storing Different sorts of Z3 expr into a map

I created a std::map of z3::expr and int pair, and wanted to store different expressions. However, when I was storing expression of different kinds, say first a 64-bit vector and then a 32-bit vector, compilers throwed a z3::exception and complaining invalid function application for bvslt, sort mismatch on argument at...

Bit vector expression extension in Z3

I have a 32bit bit vector expression. Somehow I want to do a signed or unsigned extension on this expression to a 64bit bit vector. Is there any API I can use?

Incorrect result with Z3 SMT and Python

I'm trying to replicate the script given by another user from this StackOverflow answer here http://stackoverflow.com/a/14551792 I have what I believe to be most of the pieces to get this to work with the python bindings, however I don't get the correct answer. Here is the python script: from z3...

Are C++ parameters :logic and :timeout deprecated in Z3 unstable branch?

For my application code, I used the following settings for z3 params for my solver z3::params p(context); p.set(":relevancy", static_cast<unsigned>(1)); p.set(":logic", QF_ABV); p.set(":timeout", timeout); solver.set(p); After updating to latest Z# unstable I got C++ exceptions essentially stating that logic and timeout are not valid parameters. I did not find any equivalent...

Polymorphic Functions in SMTLIB2 / Z3

Am I correct in understanding that one cannot create "polymorphic" functions in Z3 or SMTLIB2? e.g. I'd like to write something like: (declare-fun Prop (A) Bool) (declare-fun x1 () Int) (declare-fun x2 () Bool) (assert (and (Prop x1) (Prop x2))) (I guess I can get something like this by declaring...

Z3 Java API - ignoring an expression like a max-function

last time I asked how to define a function in the Z3 Java API. The reason was that there is no command to define a function in the Java API. The answer was to substitute the argument values of the function for the input values (Z3 Java API defining a...

Z3: Difference logic performance

I have a problem to solve that can be translated into difference logic, and rather than implementing a decision procedure, I would like to use z3 for this purpose. Nevertheless, I run a few examples and I had exponential-like runtimes (even though there is a polytime decision procedure for it)....

nuZ: What does the model say

When playing around with nuZ I stumbled upon this: (declare-fun x () Int) (declare-fun y () Int) (assert-soft (= x 1) :weight 1 :id first) (assert-soft (= y 4) :weight 3 :id first) (assert-soft (= x 2) :weight 1 :id second) (assert-soft (= y 5) :weight 3 :id second) (assert-soft...

Z3 Java API defining a function

I need your help defining a function with the Z3 Java API. I try to solve something like this (which is working fine with the z3.exe process): (declare-fun a () Real) (declare-fun b () Real) (declare-fun c () Bool) (define-fun max2 ((x Real) (y Real)) Real (ite (<= x y)...

Am I using z3 :timeout correctly with C++ interface for Linux?

I'm trying to get the z3 solver to timeout after 0.1s on this example (factoring a 32-bit product of two primes), using the C++ interface. It works on Windows (VC++ 2013), but not on Linux (CentOS 6.5), where the solver runs to completion in around 2.5s (debug build). This post...

Z3py returns unknown for equation using pow() function

Z3py returns unknown for the following simple problem using pow() function. import z3; goal = z3.Goal(); goal = z3.Then('purify-arith','nlsat'); solver = goal.solver(); x = z3.Real('x'); solver.add(x <= 1.8); solver.add(x >= 0); z = 10**x; #z = pow(10,x) returns same result solver.add(z >= 0, z <= 1.8); print solver.check() returns unknown...

Use z3 to Prove Identity of Boolean/Arithmetic Formula

I'm trying to use z3 to prove the following identity: x+y == x^y + 2*(x&y) That is, we can replace any addition with a mixture of boolean and arithmetic instructions (example taken from Chapter 2.2, Hacker's Delight). I'm using the following z3 python snippet: from z3 import * x =...

Getting a counterexample from ┬ÁZ3 (Horn solver)

Using Z3's Horn clause solver: If the answer is SAT, one can get a satisfying assignment to the unknown predicates (which, in most applications, correspond to inductive invariants of some kind of transition system or procedure call system). If the answer is unsat, then this means the exists an unfolding...

Get UNSAT Core using Z3 from .smt2 file

I need to get unsat core from z3. The contents of .smt2 file are: (set-option :produce-unsat-cores true) (set-logic QF_AUFBV ) (declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) ) ; Constraints (! (assert (bvslt (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32)...

function to get nibbles using Z3 and bitvector theory

I'm trying to learn a little about z3 and the bit vector theory. My intention is to make a function to get the nibble from a position of the bitvector This code returns the nibble: (define-fun g_nibble( (l ( _ BitVec 12)) (idx (Int)) ) ( _ BitVec 4) (ite...

Z3 solver returning unsat when formula should be satisfiable

I got a 'simple' formula that the Z3 solver (python interface) seems unable to handle. It is running for quite some time (30 minutes) and then returning unkown even though I can find a satisfying assignment by hand in under a minute. This is the formula: [Or(<uc 1.0> == 0,...

Z3 bitvector operations

How does one use the 'repeat' and 'rotate_left' bitvector operations? More generally, where can I find detailed documentation of bitvector operations in the SMT2 scripting format used by Z3? Everything I find seems to just go to tutorials, or broken links: https://github.com/Z3Prover/z3/wiki/Documentation http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html Trying to understand "repeat", "rotate_left", and "rotate_right"...

Z3:unknown result in Z3 C API

In current Z3 context,assert " try(X,i,j) = ((X[i][j] == i*j)) " is already existed.the type of X is (Array Int (Array Int Int)).try(X,i,j) is a function and return type is bool.here is the Z3 context: (kernel (forall ((Y (Array Int (Array Int Int))) (i Int) (j Int)) (let ((a!1 (=...

z3 python example example.py failing to execute (access violation)

example.py script fails to execute with an access violation when loading libz3.dll The same libz3.dll loads properly when compiled in a c program It appears to be a problem of using tls in memory::allocate() function Are there any feasible workarounds ============ Python Example Converted to C=============== xxxxxxxxxxxxxxxxxxRelevent machine detailsxxxxxxxxxxxxxxxxxxxx ++++++++++++++++++...

Z3 support for square root

I've been searching the square root functionality provided by z3. For example, for adding a constraint about a Real number x , that x*x = 2, what is the best way to encode that? I tried: (declare-const x Real) (assert (= 2 (* x x))) (check-sat) The result is unknown....

Are statistics accumulated across multiple check-sats?

Are the numbers returned by (get-info :all-statistics) accumulated across multiple calls to check-sat, and across multiple push-pop scopes? Or are they reset at each check-sat (or at push or pop)? Phrased differently, if I get statistics at various points during a run of Z3, and if a certain statistics, e.g.quant-instantiations...

z3py: Can the switch of the orders of constraints affect the performance of the Z3 SMT solver?

I am trying to improve the performance of my z3py code for making an inference. Do you think changing the sequence that the logic constraint being added to the solver might possibly help?

How do I create a constraint in Z3py to check if a list if a permutation of another?

I am a beginner in Z3py and I've been struggling with this for almost a week now... I don't find enough information to help me in tutorials out there neither a good example (of the function Exists) that can help me.

z3py: how to represent an array of integers or characters in z3py

I am new to z3py and SMT and I haven't found a good tutorial about z3py. Here is my problem setting: Given an input integer array I=[1,2,3,4,5], and an output integer array O=[1,2,4,5]. I want to infer k for the operator Delete, which deletes the element at position k in...

Getting Unsat Core in Z3 using C++, with Z3_parse_smtlib2_string

I need to use Z3_parse_smtlib2_string to parse some SMTLIB strings into Z3 using the C++ API, and the use the Z3 C++ API to find the unsat core of this. I know that there are other ways to find the unsat core as described here and here that are easier...

Z3: eliminate don't care variables

I have a test.smt2 file: (set-logic QF_IDL) (declare-const a Int) (declare-const b Int) (declare-const c Int) (assert (or (< a 2) (< b 2 )) ) (check-sat) (get-model) (exit) Is there anyway to tell Z3 to only output a=1 (or b=1)? Because when a is 1, b's value does not...

How to declare constants as distinct using the z3 c++ API

Giving for example: context ctx; sort type1 = ctx.int_sort(); sort type2 = ctx.bool_sort(); func_decl b1 = function("b1", type1, type2); expr x = ctx.int_const("x"); expr y = ctx.int_const("y"); expr z = ctx.int_const("z"); solver s(ctx); s.add(b1(x)); s.add(b1(y)); s.add(b1(z)); How can one declare x, y and z as distinct other than using: s.add(not(x==y...

nuZ: Use of soft-assertions with weights and ids

When playing around with nuZ I stumbled upon this: (declare-fun x () Int) (declare-fun y () Int) (assert-soft (= x 1) :weight 1 :id first) (assert-soft (= y 4) :weight 3 :id first) (assert-soft (= x 2) :weight 1 :id second) (assert-soft (= y 5) :weight 3 :id second) (assert-soft...

Verification condition of an if-else and while loop in Z3

I'm learning Z3 and want to input some verification condition as stated by the Hoare logic and obtain a model of the given Hoare triples. So far I have only been able to verify assignments, here is an example (just to check if I'm doing it right): Given: { x<...

Solver for recursive Horn clauses

These days, in automated program verifications, it is fashionable to pose problems as the solution to a system of Horn clauses, where most Horn clauses define the inductiveness conditions for an invariant, and then some constraint define the safety conditions to match. One file format for this is SMT-LIB: the...

Unexpected effect of smt.arith.nl.gb on reasoning with (syntactic) equality - bug?

Consider the following SMTLIB program (on rise4fun here): (set-option :auto_config false) (set-option :smt.mbqi false) (set-option :smt.arith.nl.gb false) (declare-const n Int) (declare-const i Int) (declare-const r Int) (assert (= i n)) (assert (= r (* i n))) (push) (assert (not (= r (* n n)))) (check-sat) ; unknown (pop) Although it...

Checkpoint mechanism for Z3

I am planning to do some work with the Z3 SMT solver from Microsoft Research that will run on a compute server with an execution time limit. I expect that the job will exceed this limit. The recommended policy for this computing center is to use "checkpoints" and to invoke...