CVC5 Parser Unable to Parse fp.as_ieee_bv

[baierd]

CVC5 can not parse the SMTLIB2 keyword fp.as_ieee_bv;

Exception in thread "main" java.lang.IllegalArgumentException: Error parsing with CVC5: Symbol 'fp.as_ieee_bv' not declared as a variable
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaManager.parseCVC5(CVC5FormulaManager.java:164)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaManager.parseImpl(CVC5FormulaManager.java:88)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaManager.parseImpl(CVC5FormulaManager.java:38)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.parse(AbstractFormulaManager.java:330)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.translateFrom(AbstractFormulaManager.java:488)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.translateFrom(FormulaManagerView.java:1907)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.SeparateInterpolatingProverEnvironment.convertToItp(SeparateInterpolatingProverEnvironment.java:122)

Commandline to trigger in CPAchecker: bin/cpachecker --no-output-files --heap 2000M --bmc-interpolation --option imc.fallBack=false --option solver.solver=MATHSAT5 --option solver.interpolationSolver=CVC5 --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --timelimit 60s --stats --spec test/programs/benchmarks/properties/unreach-call.prp --32 test/programs/benchmarks/float-benchs/inv_Newton.c.p+cfa-reducer.c
(Note: using JavaSMT from the CVC5 parser branch!)

FP to IEEE-BV support for CVC5 is not yet merged, but should be parsable regardless (see #514).

TODO:

• is this keyword used correctly by MathSAT5 in the export?
• is an option or any other special handling required by CVC5 to parse this?
• contact CVC5 devs to ask for support.

[baierd]

This is a general limitation of SMTLIB2.

Some solvers offer support for this, some don't. In general one should not trust this conversion though, as there are multiple interpretations for special numbers!

PR 512 extends JavaSMT with a general method to avoid the problem.