1

Closed

Assert labels not freed on pops.

description

Hi guys,

I use z3 (4.3.1) with smt lib 2 input. A simple example follows. I admit the example seems pointless, but I noticed it when extrapolating a model of a formula in a variation of the QE algorithm by Monniaux using unsat core to try to further reduce the extrapolant when getting an unsat result (in a SMT-test-like algorithm where the atoms of the formula are removed one by one: generalize2 in http://www-verimag.imag.fr/~monniaux/biblio/Monniaux_LPAR08.pdf).

Of course, a simple workaround is to increment a counter to make sure that there is no collision between the labels, but it does feel like a bug doesn't it?

Thank you in advance.

Adrien

(set-option :print-success true)
(set-option :produce-unsat-cores true)

(declare-fun a () bool)
(declare-fun b () bool)
(assert (! a :named A))
(assert (! (not b) :named notB))
(check-sat)
; sat

(push 1)
(assert (! (not a) :named notA))
(check-sat)
; unsat
(get-unsat-core)
; (A notA)

(pop 1)
(assert (! (not a) :named notA))
; (error "line 19 column 20: named expression already defined")`
`

file attachments

Closed Jun 11, 2013 at 8:39 PM by leodemoura
This is not a bug. You should use the option http://rise4fun.com/Z3/QlTr for getting the desired behavior

comments

leodemoura wrote Jun 11, 2013 at 8:38 PM

You should use the option (set-option :global-decls false)
Then, all "names" and declarations will be scoped.

Here is the updated example: http://rise4fun.com/Z3/QlTr