Z3, Theorem Prover

Welcome to Z3 Forum

Leonardo de Moura — Tue, 08 Jan 2008 20:17:03 GMT

Z3 forum is intended for general discussions involving Z3, as well as announcements of new tools, language changes, etc.

The Z3 website is located at: http://research.microsoft.com/projects/z3/

How to enable predicate labeling in SMTLIB format?

jasonweiyi — Fri, 20 Nov 2009 08:37:13 GMT

Does Z3 support predicate labeling in SMTLIB file?

We tried to write labels, but Z3 seems to ignore all of them.

Z3 MacOS X

barbaravieira — Wed, 04 Nov 2009 09:43:38 GMT

I would like to know if there is any version of Z3 to MacOS X and where I can find it.

If there isn't any version, could you please provide one to MacOS X (Snow Leopard)?

Thank you in advance.

Z3 Unsat Core Support

sagarj — Fri, 16 Oct 2009 23:23:02 GMT

Is there a way in Z3 to output the subset of clauses which forms the unsat core given an unsatisfiable conjuction of clauses? In my case input formula is a conjunction of atomic formulas in QF_AUFBV.

It would be really great if someone can help me with my query.

Thanks,

Sagar

how to deal with this expression?

xyz031702 — Mon, 28 Sep 2009 10:45:27 GMT

Dear All

I got a problem when dealing with the following Z3 expression:

(benchmark tst :extrafuns ((V1 Real)(flag Real)) :formula (not (= (* V1 flag) flag)))

The output result is a bit strange:

potential model: V1--->0 , flag---->0

So does this mean Z3 cannot find a possible solution for it ? Is there any other similar cases? Or what is a general expression for these similar cases?

Expecting for replies ,

Thanks and best regards,

Ding Sun

how to support the following operations: &, %, |

xyz031702 — Thu, 24 Sep 2009 14:40:21 GMT

Hi, all

I am a beginner using Z3, which already helps me a lot.

However I met problems when meeting operations : &(bitwise And) , %(mod) ,|(bitwise Or)

Example:

I try to prove:

(benchmark tst :extrafuns ((a Real)) :formula (not (= (% a 2) 1)) :formula (> a 0))

(benchmark tst :extrafuns ((a Real)) :formula (not (= (& a 2) 1)) :formula (> a 0))

(benchmark tst :extrafuns ((a Real)) :formula (not (= (| a 2) 1)) :formula (> a 0))

The prover will throw exceptions saying "Error: could not find overload for '%' ".

Is there anyone knowing how to solve such problem?

Expecting for the replies and suggestions. Thanks a lot.

Ding Sun

New member need some support

YangHoun — Mon, 07 Sep 2009 17:47:24 GMT

Hello,

I'm Yang. I'm student & I have a small research about Software Verification, I search on Internet & find Z3 prover/solver. I think it is tool that i need. But in a short time, I can't handle all of API of Z3, so I have a confuse problem:

How do I write some structure such as if....else; switch...case; while; for; ... in Z3?

And how I write a programe to check a small program that is right or wrong?

Example: I have a program named "greaterValue", it return a greater value among two value (int a, int b). But I have wrong code as:

int greaterValue(int a, int b){
      int result;
      if(a>=b)
                result = a+10; // the right code must be: result = a;
      else
            result = b;
     return result;
}

//The correct expression for this program: (((x>=y)&&(max==x))||((x<y)&&(max==y)))

How I use Z3 to recognize this code is wrong & generate counter-example to illustrate.

Thank you very much.

Yang. H

Cardinality constraints

kornevgen — Thu, 17 Sep 2009 20:40:46 GMT

Hi!

I try to use cardinality constraints but Z3 doesn't solve my constraints:

(benchmark test
:logic QF_BV

:extrafuns ((x BitVec[5]) (y1 Int) (y2 Int))

:assumption
(= y1 (ite (= (extract[2:0] x) bv1[3]) 1 0) )

:assumption
(= y2 (ite (= (extract[4:2] x) bv1[3]) 1 0) )

:assumption
(<= 2 (+ y1 y2))

)

And Z3 2.1 returns the following model:

x -> bv1[5]
y1 -> 1
y2 -> 0
sat

However these constraints must be UNSAT ! because it doesn't exist "x" such as x[4:2] == 1 and x[2:0] == 1.

How my constraints can be corrected ?

How do I represent the control and loop structures using Z3

KimYLee — Wed, 09 Sep 2009 10:22:20 GMT

Hello,

How do I represent some control and loop structures such as:
if...else;
for();
while();

by using Z3 ???

Thanks

Lee, Kim

Using C API with Visual C++ 6 issue?

cosinepi — Wed, 26 Aug 2009 15:15:52 GMT

Hi all,

I just started with Z3 for a few days.

I have Visual Studio 6 Enterprise Edition on my lab machine, on a 32bit WinXP platform.

I downloaded Z3 2.1, installed, and am now trying to run the examples in the 'examples\c' directory. When I type 'build.cmd' in this directory, the following errors are given:

C:\Program Files\Microsoft Research\Z3-2.1\examples\c>cl /I ..\..\include ..\..\bin\z3.lib test_capi.c
Microsoft (R) 32-bit C/C++ Optimizing Compiler Version 12.00.8168 for 80x86
Copyright (C) Microsoft Corp 1984-1998. All rights reserved.

test_capi.c
..\..\include\z3_api.h(2183) : error C2632: 'long' followed by 'long' is illegal
..\..\include\z3_api.h(2195) : error C2632: 'long' followed by 'long' is illegal
..\..\include\z3_api.h(2453) : error C2632: 'long' followed by 'long' is illegal
..\..\include\z3_api.h(2453) : error C2632: 'long' followed by 'long' is illegal
..\..\include\z3_api.h(2488) : error C2632: 'long' followed by 'long' is illegal
..\..\include\z3_api.h(2501) : error C2632: 'long' followed by 'long' is illegal

C:\Program Files\Microsoft Research\Z3-2.1\examples\c>

Similar error happens when I copy the files bin\z3.dll, bin\z3.lib, include\z3.h, and include\z3_api.h into my program folder and #include "z3.h".

I delved into the z3_api.h file and found that these lines are surrounded within the #ifndef CAMLIDL...#endif block. I then added the /D "CAMLIDL" switch to the build command that I use, then another syntax error at line 914 of z3_api.h arises. The surrounding lines there are

#ifndef CAMLIDL
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
#else
[pointer_default(ref)] interface Z3 { // line 914 of z3_api.h
#endif // CAMLIDL

The syntax error just reports a '['.

Is there any hint why this happens and how to fix it? Thank you in advance! (BTW, the .NET API examples are working fine. However for some reason I can only use C API's.)

--Vincent

Why is it SAT ?

kornevgen — Mon, 20 Jul 2009 06:50:45 GMT

Good day!

Z3 says the following smt is SAT

(benchmark xx
:logic QF_BV
:extrafuns ((x Int))
:assumption
(and (> x 0) (< x 1) )
)

with model "x -> val!0"

Yes, this code has an error: the correct logic is QF_LIA but not QF_BV (Z3 says UNSAT with QF_LIA and it is correct, of course). So, my question is what means "val!0" ? some unknown 0'th value ?

Does Z3 performs modular checks (or method-scope checks, or...)?

ElenaPavlova — Sun, 14 Jun 2009 08:43:35 GMT

Greetings,

the question is

how deep does Z3 considers c#+spec# code paths when verifying it?

that is - are method constraints (''ensures'' for example) verified within the method they are declared in, considering external function calls using only their pre- and post- conditions? Or these external functions are also considered in detail (including possible execution paths)

or within a module, when dealing with, for example, class invariants:

does Z3 verifies class invariants within the module scope using constraints for description of interaction with external modules? Or it uses the full system (program) description to verify any property?

Information on "Z3,Theorem Prover"

Hernan Weintraub — Wed, 01 Jul 2009 16:32:10 GMT

Hello to All

Where I can find Articles about this Subject("Z3,Theorem Prover") ?

I do not understand the meaning of "Theorem Prover".

The main target of this is to develope some tools that will Prove some Mathematical Theorems in a Computer(Artificial Intelligence).

I saw in the forum that it has a connection to sound but in somewhere else I saw a connection to Algorithms.

Sorry about my Ignorance.

Many Thanks

Hernan

Signed Bitvectors, confused about extending and extraction

Menno — Wed, 10 Jun 2009 16:01:11 GMT

I was wondering why the following AST is unsat:

(= (extract 31 0 (sign_extend 32 -5)) -5)

-5 has a bitvector type of size 32, which is then sign extended it to a bitvector of size 64 and then the 32 lower bits are extracted. I thought that the resulting bitvector should be equal to the original bitvector.
Note that this example returns sat for positive bitvectors.

Bit-vector concat operator being ignored?

SeanHn — Wed, 10 Jun 2009 12:31:20 GMT

Hey guys,

I'm trying to express the condition gathered from a conditional jump. My program instrumentation is performed at the byte level so in the case of a conditional based on a word or dword I need to concatenate the constituent bytes into a new variable before making the comparison. It is this concatenation that is giving trouble. The following is a quick test I just wrote to see how the concat operator worked.

I am aiming to make the formula unsatisfiable by constraining i0 and i1 to 0 and then expressing c1 as the concatenation of these variables; I then ask the solver if it is possible for c1 to equal 22. (I'm using the latest public version of Z3 for Windows)

(benchmark test

:status unknown

:logic QF_BV

:extrafuns ((i0 BitVec)(i1 BitVec)(c1 BitVec[16]))

:assumption (and (= i0 bv0)(= i1 bv0)(concat i0 i1 c1))

:formula ((= c1 bv22[16])) )

Z3 tells me this is satisfiable, and the model it returns is as follows:

partitions:

*2 (i1 i0) -> 0:bv8

*3 (c1) -> 22:bv16

Which seems to indicate it isn't considering the effect of restricting i0/i1 to 0 when assigning a value to c1. Is there something obviously wrong with the SMT-LIB input I'm using? Or am I misinterpreting how to use 'concat'?

Thanks for your time, Sean

Z3 - getting started. Z3 seems to ignore my constraints

ElenaPavlova — Tue, 19 May 2009 09:07:40 GMT

Greetings,

I was expirementing with Z3 in Visual Studio 2008 IDE.

here is a simple C# code with an ensures constraint

public class testClass

{

public int testMethod ()

ensures 3>4;

{ return 2;}

}

As far as I understood, IDE Build command should try to verify and compile this code and issue warnings or errors -

because the constraint never holds. Unfortunately it didn't show any. I suppose Z3 was installed successfully and is working for it shows "reciever might be null warnings" for the Bag class given in examples and articles.

Where am I wrong? may be z3 was installed incorrectly? may be I try to use Z3 for things it isn't intended for?

Thank you

P.S. Probably this should be in the spec# forum, sorry

Type Conversion bitvector <-> real and some remarks about the C api

Menno — Tue, 09 Jun 2009 09:59:43 GMT

I am currently developing an concolic (like PEX) test data input generator for Java as part of my Master's project.

Bitvectors belong to a different theory than reals. Hence, it is impossible to compare bitvector types and real types directly. In programming languages it is possible to cast integer variables to float variables. What would be the best strategy to convert these types in the constraint solver?

Option 1:

I could use the concrete value that is collected while running the program with concrete input. For example, if an float is casted to a integer, then we would use the result of this conversion to initialize the variable in the constraint solver. However, this approach loses the `link' between the integer constraints and real constraints.

Option 2:

Alternatively, I could use a set of constraints to convert between bitvectors and reals. The following pseudo C code fragments convert between bitvectors and reals. Note that this is very similar to how integers and floats are converted.

Conversion from bitvector b to real r:

int b;
real r;
//this loop is unrolled:
for (int i = 0; i < bvsize(b); i++) {
    int x_int = 1 << i; //precomputed
    real x_real = 1 << i; //precomputed
    if (b & x_int) {
        r += x_real;
    }
}

Conversion from positive real r to bitvector b:

real r;
int b;
if (MAXVALUE(b) <= r) {
    r = MAXVALUE(b);
}
if (r <= MINVALUE(b)) {
    r = MINVALUE(b);
}
if (MINVALUE(b) < r < MAXVALUE(b)) {
    //this loop is unrolled:
    for (int i = 0; i < bvsize(b); i++) {
        int x_int = 1 << bvsize(b) - i; //precomputed
        real x_real = 1 << bvsize(b) - i; //precomputed
        if (r > x_real) {
            b = b & x_int;
            r = r - x_real;
        }

}
}

- Would performance suffer considerably if I use this second approach? And are there perhaps better approaches?

Is Z3 sound?

ElenaPavlova — Sun, 07 Jun 2009 08:05:38 GMT

I haven't understood from the articles, sorry

but is Z3 sound?

MUC in Z3

schaef — Fri, 06 Feb 2009 14:37:46 GMT

Hi there, currently i am working with a bunch of unsat formulas and i am wondering if there is a way to get the minimal unsatisfiable core of a formula from z3? greets, martin

Is this a bug with the C API?

bdclark — Fri, 06 Mar 2009 12:30:11 GMT

Hello,

I was experimenting with Z3 by using the C API, when I noticed that the generated model did not satisfy the supplied constraints. I have pasted the contents of a C file demonstrating the problem, along with the runtime output, below. Is there a bug somewhere, or do I not understand what Z3 does for model generation?

Is it possible to generate a model which complies with the supplied constraints? If so, how should it be done?

Source Code:

#include <z3.h>

int main( int argc, char* argv[] )
{
    //Setup Z3
    Z3_config cfg = Z3_mk_config();
    Z3_set_param_value(cfg, "MODEL", "true");
    Z3_context ctxt = Z3_mk_context(cfg);
    Z3_del_config(cfg);

    //Create symbols and variables
    Z3_type_ast real = Z3_mk_real_type(ctxt);
    Z3_symbol symbol_X = Z3_mk_string_symbol(ctxt, "X" );
    Z3_symbol symbol_Y = Z3_mk_string_symbol(ctxt, "Y" );
    Z3_symbol symbol_a = Z3_mk_string_symbol(ctxt, "a" );
    Z3_symbol symbol_b = Z3_mk_string_symbol(ctxt, "b" );
    Z3_symbol symbol_c = Z3_mk_string_symbol(ctxt, "c" );
    Z3_symbol symbol_d = Z3_mk_string_symbol(ctxt, "d" );
    Z3_symbol symbol_t = Z3_mk_string_symbol(ctxt, "t" );
    Z3_symbol symbol_u = Z3_mk_string_symbol(ctxt, "u" );
    Z3_ast X = Z3_mk_const(ctxt, symbol_X, real);
    Z3_ast Y = Z3_mk_const(ctxt, symbol_Y, real);
    Z3_ast a = Z3_mk_const(ctxt, symbol_a, real);
    Z3_ast b = Z3_mk_const(ctxt, symbol_b, real);
    Z3_ast c = Z3_mk_const(ctxt, symbol_c, real);
    Z3_ast d = Z3_mk_const(ctxt, symbol_d, real);
    Z3_ast t = Z3_mk_const(ctxt, symbol_t, real);
    Z3_ast u = Z3_mk_const(ctxt, symbol_u, real);

    //Convenience functions
    Z3_ast add2(Z3_ast lhs, Z3_ast rhs) {
        const Z3_ast args[2] = {lhs,rhs};
        return Z3_mk_add(ctxt,2,args);
    }
    Z3_ast sub2(Z3_ast lhs, Z3_ast rhs) {
        const Z3_ast args[2] = {lhs,rhs};
        return Z3_mk_sub(ctxt,2,args);
    }
    Z3_ast mult2(Z3_ast lhs, Z3_ast rhs) {
        const Z3_ast args[2] = {lhs,rhs};
        return Z3_mk_mul(ctxt,2,args);
    }

    //Create logic constraints
    Z3_ast show = NULL;

    show = Z3_mk_eq(ctxt,add2(t,u),Z3_mk_numeral(ctxt,"1",real));
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_eq(ctxt,c,t);
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_eq(ctxt,d,u);
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_eq(ctxt,a,u);
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_eq(ctxt,b, sub2(Z3_mk_numeral(ctxt,"0",real),t));
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_le(ctxt, add2(mult2(X,c),mult2(Y,d)), Z3_mk_numeral(ctxt,"10",real) );
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_ge(ctxt, add2(mult2(X,c),mult2(Y,d)), Z3_mk_numeral(ctxt,"5",real) );
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show = Z3_mk_le(ctxt, add2(mult2(X,a),mult2(Y,b)), Z3_mk_numeral(ctxt,"10",real) );
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    show=Z3_mk_ge(ctxt, add2(mult2(X,a),mult2(Y,b)), Z3_mk_numeral(ctxt,"5",real) );
    Z3_assert_cnstr(ctxt,show);
    printf("%s\r\n",Z3_ast_to_string(ctxt,show));

    //Check and show results
    Z3_model model;
    Z3_lbool result = Z3_check_and_get_model(ctxt,&model);

    printf("\r\nResult=%s\r\n\r\n",
        result==Z3_L_FALSE?"False": (result==Z3_L_TRUE?"True":"Undefined") );

    if( !model )
        printf("No model generated.\r\n");
    else {
        printf("%s\r\n",Z3_model_to_string(ctxt,model));
        Z3_del_model(model);
    }

    Z3_del_context(ctxt);

    return 0;
}

Output:

(= (+ t u) 1)
(= c t)
(= d u)
(= a u)
(= b (- 0 t))
(<= (+ (* X c) (* Y d)) 10)
(>= (+ (* X c) (* Y d)) 5)
(<= (+ (* X a) (* Y b)) 10)
(>= (+ (* X a) (* Y b)) 5)

Result=True

partitions:
*2 {t c b Y X} -> 0:real
*3 {u d a} -> 1:real

I expected to see that the constraint "(>= (+ (* X c) (* Y d)) 5)", which should be "(X*c)+(Y*d) >= 5", would evaluate to be true when substituting the results from the model. From the resulting model, "X", "Y", and "c" are all 0, and then "d" is 1. Through substitution, the constraint evaluates to "(0 * 0)+(0 * 1) >= 5", which is false. Is this correct?

Simplify format and tuple theory

Bruce M. A. — Sun, 15 Mar 2009 20:40:06 GMT

Is it possible to deal with tuples in Z3 with the Simplify format? I've tried what I would consider the more likely possibilities for functions, i.e. mk_tuple, tuple, etc., but nothing so far.

using simplify input format

schaef — Wed, 04 Mar 2009 14:58:02 GMT

i've got some problems with the simplify input format. i have a quit large let expression (e.g. LET a b) which is used in a bunch of formulas of the form (IMPLIES c (LET a b)) where c shares some variables with a.

now i thought that i could push the LET expression using BG_PUSH instead of copying it each time i check one of these implications. so far was not not able to write this using the simplify format.

Any hint how to do this?

Thanks,

Martin

C API - Getting Started

benjnorthrop — Thu, 05 Jun 2008 19:38:24 GMT

Hello - I apologize up-front for the newbie question. I'm trying to get started using the Z3 C API, and am looking for documentation for getting the environment situated, building, linking, and executing programs which use this API. I'm on a windows machine and have LCC, but also Cygwin with GCC. Any intro information would be extremely helpful.

Thanks very much.

-Ben

How can I rewrite this in smt-lib syntax?

Ewunia — Sat, 17 Jan 2009 03:39:45 GMT

I know Simplify and in Simplify syntax I can create recursive functions such as:

(BG_PUSH (EQ (factorial 1) 1))
(BG_PUSH (FORALL (n ) (IMPLIES (> n 1) (EQ (factorial n) (* (factorial (- n 1)) n)))))
(EQ (factorial 5) 120)

When I feed Z3 with Simplify syntax it returns Valid.

How can I rewrite this in SMT-LIB format?

Thank you

is it possible with Z3?

olfa — Tue, 23 Dec 2008 18:50:44 GMT

Hello Z3 community,
I want to know if Z3 could solve a system of equations like this example:
solve(x+Sum[A[k],k=i..N]==y+Sum[B[k],k=m..N],
j-Length==l-Length,
z/(c ^ i)==t/(c ^ h),
u+1==2*v-3w,

v=f(f(w)))

(here A and B are arrays; C et D are lists;
x,y,z,t,j,l,i,h,u,v,w are variables that could be of type integer or real, c is a constant and f is a function):

Thank you very much.