SMT2 Parsing crash: `java.lang.UnsupportedOperationException: Bound variables are no longer explicitly visited in JavaSMT. Use a combination of 'visitQuantifier' (for the whole quantified formula) and 'visitFreeVariable' (in the body) instead.`

[Bixilon]

Hi,

I am trying to parse fault_free_convergence_000.smt2 using `FormulaManager::parseAll(String):

FormulaManager formulaManager = context.getFormulaManager();
List<BooleanFormula> formulas = formulaManager.parseAll(input);

Sadly it is crashing with:

Exception in thread "main" java.lang.UnsupportedOperationException: Bound variables are no longer explicitly visited in JavaSMT. Use a combination of 'visitQuantifier' (for the whole quantified formula) and 'visitFreeVariable' (in the body) instead.
        at org.sosy_lab.java_smt.api.visitors.FormulaVisitor.visitBoundVariable(FormulaVisitor.java:52)
        at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:403)
        at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:77)
        at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:316)
        at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visitRecursively(FormulaCreator.java:347)
        at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visitRecursively(FormulaCreator.java:332)
        at org.sosy_lab.java_smt.basicimpl.FormulaCreator$VariableAndUFExtractor.visitQuantifier(FormulaCreator.java:486)
        at org.sosy_lab.java_smt.basicimpl.FormulaCreator$VariableAndUFExtractor.visitQuantifier(FormulaCreator.java:425)
        at org.sosy_lab.java_smt.basicimpl.RecursiveFormulaVisitorImpl.visitQuantifier(RecursiveFormulaVisitorImpl.java:83)
        at org.sosy_lab.java_smt.basicimpl.RecursiveFormulaVisitorImpl.visitQuantifier(RecursiveFormulaVisitorImpl.java:27)
        at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visitQuantifier(PrincessFormulaCreator.java:529)
        at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:399)
        at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visit(PrincessFormulaCreator.java:77)
        at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:316)
...
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visitRecursively(FormulaCreator.java:347)
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visitRecursively(FormulaCreator.java:332)
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.extractVariablesAndUFs(FormulaCreator.java:420)
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.extractVariablesAndUFs(FormulaCreator.java:396)
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.parseStringToTerms(PrincessEnvironment.java:330)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaManager.parseAllImpl(PrincessFormulaManager.java:74)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.parseAll(AbstractFormulaManager.java:473)
	at org.sosy_lab.java_smt.cmdline.JavaSMTMain.run(JavaSMTMain.java:179)
	at org.sosy_lab.java_smt.cmdline.JavaSMTMain.main(JavaSMTMain.java:99)

[daniel-raffler]

Hello,

I had a look at it, and the issue seems to be caused by epsilon terms. Princess will often rewrite terms, and in this case it turns (/ 1.0 2.0) into the following epsilon term:

EPS [Rat]. EX [Rat]. EX [Rat}.
 (((_1[Rat] = Rat_div(Rat_fromRing(1), Rat_fromRing(1))) &
   (_0[Rat] = Rat_div(Rat_fromRing(2), Rat_fromRing(1)))) &
   (_2[Rat] = \if ((_0[Rat] = Rat_fromRing(0)))
      \then (ratDivZero(_1[Rat]))
      \else (Rat_div(_1[Rat], _0[Rat]))))

Unfortunately SMTLIB doesn't support epsilon terms, and neither does JavaSMT. I had written a PR some time ago to "backtranslate" the transformation, but it's pretty outdated now, and I'm not sure if this is really the best way to solve it

If you just want to parse the term, maybe the best solution is to just ignore the epsilon variable here. However, this will probably cause issues if you want to use the visitor for any transformation later

@baierd Do you have any ideas how to best fix this?

Here's a short test to reproduce the crash:

  @Test
  public void princessBug() {
    var out = mgr.parse("(assert (> 0.0 (/ 1.0 2.0)))");
    System.out.println(out);
  }

[daniel-raffler]

@Bixilon I've added a workaround on this branch. Could you check if it solves the issue for you?

[Bixilon]

@daniel-raffler Indeed, seems to solve it (or at least it is not crashing anymore). Did not verify the results (yet).