OpenSMT reports error on the following example, which is deemed valid by other solvers, such as z3 and cvc5.
(set-logic QF_LIA)
(declare-fun o () Int)
(declare-fun i () Bool)
(push 1)
(assert (! (< o 0) :named c0))
(pop 1)
(assert (! i :named c0))
(check-sat)
The problem is, that OpenSMT does not remove term names from its context after pop, and when reusing the name c0, it reports an error, because the it remembers the first use of c0 in its context.
OpenSMTreports error on the following example, which is deemed valid by other solvers, such asz3andcvc5.The problem is, that
OpenSMTdoes not remove term names from its context afterpop, and when reusing the namec0, it reports an error, because the it remembers the first use ofc0in its context.