Princess: "Unknown formula type" in 2026-05-20

[daniel-raffler]

Hello,

with Princess 2026-05-20 there is a single crash caused by an unknown formula type:

bin/cpachecker --bmc-interpolation --option cpa.predicate.encodeFloatAs=unsupported --option solver.solver=princess --spec test/programs/benchmarks/properties/unreach-call.prp --32 test/programs/benchmarks/verifythis/lcp.c

Exception in thread "main" java.lang.IllegalArgumentException: Unknown formula type 'class ap.parser.IConstant' of sort 'any' for formula '__JAVASMT__BOUND_VARIABLE_15'.
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaType(PrincessEnvironment.java:575)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.getFormulaType(PrincessFormulaCreator.java:282)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.getFormulaType(PrincessFormulaCreator.java:77)
	at org.sosy_lab.java_smt.basicimpl.FormulaCreator.encapsulateWithTypeOf(FormulaCreator.java:217)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.visitQuantifier(PrincessFormulaCreator.java:532)
	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$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.AbstractFormulaManager.extractVariables(AbstractFormulaManager.java:611)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.extractVariableNames(FormulaManagerView.java:1531)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.InterpolationHelper.recordInterpolantStats(InterpolationHelper.java:236)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.reachFixedPointByInterpolation(IMCAlgorithm.java:861)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.reachFixedPoint(IMCAlgorithm.java:772)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.interpolationModelChecking(IMCAlgorithm.java:605)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.run(IMCAlgorithm.java:544)
	at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:549)
	at org.sosy_lab.cpachecker.core.CPAchecker.run0(CPAchecker.java:407)
	at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:312)
	at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:157)
Caused by: java.lang.IllegalArgumentException: Unknown formula type 'class ap.types.Sort$$anon$1' for sort 'any'.
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaTypeFromSort(PrincessEnvironment.java:612)
	at org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.getFormulaType(PrincessEnvironment.java:570)
	... 31 more

This is likely a problem with our visitor, and not Princess itself