Sort symbol name is not cleared after pop

[rainoftime]

Hi, for the formula below

(set-logic QF_UF)
(push 1)
(push 1)
(declare-sort S3 0) 
(pop 1)
(declare-sort S3 0)
(pop 1)
(check-sat)

opensmt 6518bf9

(error "sort S3 already declared")

The symbol S3 should have been cleared after the first pop operation. Or is this because opensmt restricts that a sort name should at most be used once?

[rainoftime]

(set-logic QF_UFLRA)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(define-fun _1334 () Real (__BASE_ADDRESS_OF__ 0.0))

/Logic.cc:981: PTRef Logic::mkUninterpFun(SymRef, const vec<PTRef>&): Assertion `isUFTerm(tr) || isUP(tr)' failed.
Aborted

[blishko]

(set-logic QF_UFLRA)

Hi @rainoftime! Unfortunately, OpenSMT does not support theory combination at the moment, so logics like QF_UFLRA will not work. We will try to provide an error message for this, instead of the situation you get now.

[blishko]

(error "sort S3 already declared") The symbol S3 should been cleared after the first pop operation. Or is this because opensmt restricts that a sort name should at most be used once?

I think that's the case, maybe @aehyvari can comment on this more, but I believe the OpenSMT at the moment does not clear defined symbols after pop. I am also afraid we will not have time to address this issue in the near future. Unless of course there is a use case that requires this.