z3: adding variable declarations in the assertions

Question

Is there a way to add the function definitions as assertions in the solver?

I am currently working on bounded model checking of C++ files and being able to add the definitions as assert statements will provide sort of a one to one correspondence to solver assertion and line of code.

For example I have the following toy program:

int x, y;
x = y + 1;
assert(x != 0)

CBMC produces the following smt2 file:

(declare-fun |main::1::y!0@1#1| () (_ BitVec 32))
(define-fun |main::1::x!0@1#2| () (_ BitVec 32) (bvadd (_ bv1 32) |main::1::y!0@1#1|))
(define-fun |B0| () Bool (= |main::1::y!0@1#1| |main::1::y!0@1#1|))
(assert (not (not (= |main::1::x!0@1#2| (_ bv0 32)))))

z3_parse_string returns the following formula.

Not(Not(1 + main::1::y!0@1#1 == 0))

I was wondering whether it is possible to add the function declarations into the solver as well, something along the lines of:

(x!0@1#2 == 1 + y!0@1#1) AND !(x!0@1#2 == 0)

So each clause corresponds loosely to one line of source code.

I understand that currently the z3_parse_string api only access the (assert... lines and does folding from there (please correct me if I am wrong) The only solution I can think of is modifying the file such that the define-fun becomes declare-fun and the definition is pushed into a new assertion line like:

(declare-fun |main::1::x!0@1#2| () (_ BitVec 32))
(assert (= |main::1::x!0@1#2| (bvadd (_ bv1 32) |main::1::y!0@1#1|)))

Many thanks in advance.

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2016-04-08T16:44:44

Without seeing more examples or actual code (CBMC or Z3) I don't have a better solution either. In general, I would discourage people from using Z3_parse_string altogether, it often creates more confusion than necessary. It's better to either switch to full SMT2-files via the command line, or go all the way and translate the problem into Z3-API calls (excluding string parsing etc). Last I checked, CBMC had an API backend for Z3, so that should be pretty straightforward.

z3: adding variable declarations in the assertions

1 Answers