Assertion violation at smtrat-solver/Manager.cpp:163

[rainoftime]

Hi, for the following formula,

(set-logic QF_LRA)
(declare-fun v5 () Bool)
(push 1)
(declare-fun v6 () Bool)
(assert (and v6 v5))
(pop 1)

smtrat (commit 3f50332) throws an assertion violation

smtrat-static: /home/peisen/test/tofuzz/smtrat/src/smtrat-solver/Manager.cpp:163: smtrat::ModuleInput::iterator smtrat::Manager::remove(smtrat::ModuleInput::iterator): Assertion `_subformula != mpPassedFormula->end()' failed.

[nafur]

I had a quick look here. It seems that the ModuleInput splits the (and ...) into the two subformulae and remove() simply searches for the formula, but does not do the splitting.