AssertionError in SmtInterpol(SmtInterpol other, ...) constructor.

[Confectio]

While running the tests testMusEnumerationScriptSet2" or "testMusEnumerationScriptSet5" in MusesTest.java, an error occurred in the SmtInterpol(SmtInterpol other, , final Map<String, Object> options, final OptionMap.CopyMode mode) constructor:

java.lang.AssertionError
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTracker.buildProof(ProofTracker.java:54)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTracker.auxAxiom(ProofTracker.java:206)
at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.setupCClosure(Clausifier.java:1764)
at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.setLogic(Clausifier.java:1822)
at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.setupClausifier(SMTInterpol.java:601)
at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.(SMTInterpol.java:346)
at de.uni_freiburg.informatik.ultimate.smtinterpol.muses.MusEnumerationScript.executeReMus(MusEnumerationScript.java:273)
at de.uni_freiburg.informatik.ultimate.smtinterpol.muses.MusEnumerationScript.getUnsatCore(MusEnumerationScript.java:236)
at de.uni_freiburg.informatik.ultimate.smtinterpol.muses.MusesTest.testMusEnumerationScriptSet2(MusesTest.java:1295)

I made a commit, for easy reproducibility(, since in the latest commits I have built in a workaround):
0df07cc
In this commit, you only have to run "testMusEnumerationScriptSet2" or "testMusEnumerationScriptSet5" in MusesTest.java to reproduce the error.

Helpful Information:
An easy workaround is to set the option SMTLIBConstants.PRODUCE_PROOFS to true BEFORE calling this constructor.
A weird thing is, despite having SMTLIBConstants.PRODUCE_PROOFS set to true in the given Map<String, Object> for the constructor, the error still occurs, if SMTLIBConstants.PRODUCE_PROOFS is not set to true before the call.

Basically, the error seems to occur, because in ProofTracker.auxAxiom, getFunctionWithResult is called and this does not find the function @tautology, therefore returns null. In another setting, that also uses the constructor (execute getUnsatCore of SMTInterpol with the same terms asserted etc., but SMTInterpolOptions.UNSAT_CORE_CHECK_MODE set to true, without having set SMTLIBConstants.PRODUCE_PROOFS to true), it finds the function @tautology in mDeclaredFuns.

Tanja concluded, that this Error has something to do with the usage of ProofTracker instead of the interface IProofTracker.
(I don't know who will be debugging this, so if it is not Tanja, you might want to talk to Tanja for more information about this)