Popping multiple scopes at once leads to AssertionError in `CCTerm.unshare`

[sallaigy]

Hello,

The following script crashes SMTInterpol with an AssertionError:

(set-logic LIA)
(push)
(declare-fun b () Int)
(assert (exists ((e Int)) (= b e)))
(push)
(push)
(pop)
(pop)
(push)
(assert (< 0 b))
(pop 2)

This is the stack trace:

Exception in thread "main" java.lang.AssertionError
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.unshare(CCTerm.java:292)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.pop(Clausifier.java:2343)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.pop(SMTInterpol.java:413)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2822)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1333)
    at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:120)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:99)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:182)

Changing the last (pop 2) into a two (pop 1)'s allows us to avoid the crash, so it seems to be related to the behavior of the solver when trying to pop multiple scopes at once.

[damien-zufferey-sonarsource]

I think the bug comes from the engine and the theory part getting out of sync when poping with n > 1.

--- a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/convert/Clausifier.java
+++ b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/convert/Clausifier.java
@@ -2333,8 +2333,8 @@ public class Clausifier {
                mWarnedInconsistent = false;
                numpops -= mNumFailedPushes;
                mNumFailedPushes = 0;
-               mEngine.pop(numpops);
                for (int i = 0; i < numpops; ++i) {
+                       mEngine.pop(1);
                        mCCTerms.endScope();
                        /* unshare all ccterms that are no longer shared with LA but were in the previous scope */
                        for (final Term term : mLATerms.undoMap().keySet()) {

This seems to fix it. @sallaigy can you try?

[sallaigy]

I can confirm this change fixes the issue on my side with the script above.

[jhoenicke]

I think I understand the problem now. The mEngine.pop() will also invoke pop on the Theories, so when the loop starts the theories will already have removed two push/pop-levels. In the first iteration of the loop a shared term is unshared, since it still exists on the lower level, but is no longer shared. However, the congruence closure has already removed the term, since it has both levels already removed. So we try to unshare a term that no longer exists and this fails an assertion.

I wonder if it's better to not automatically unshare terms when they are removed. Having the sharedTerm set in a ccterm that is no longer in the E-Graph shouldn't be an issue at all. It's hard to find a clean solution, since the Clausifier and the Theories are so closely interwoven (the Clausifier is really the Theory-Combination).

[jhoenicke]

I added a small change to not unshare the terms in the removeTerm() function. This solves the problem.