This project is read-only.


Assert labels not freed on pops.


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

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.


(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))
; sat

(push 1)
(assert (! (not a) :named notA))
; unsat
; (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 9:39 PM by leodemoura
This is not a bug. You should use the option for getting the desired behavior


leodemoura wrote Jun 11, 2013 at 9: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: