Princess: fix name detection for BV operations like `BV_ULE`.
Previously, the function name was set to the complete String representation of the formula.
@@ -211,8 +211,10 @@ class PrincessFormulaCreator
}
private String getName(IExpression input) {
- if (input instanceof IAtom || input instanceof IConstant) {
- return input.toString();
+ if (input instanceof IAtom) {
+ return ((IAtom) input).pred().name();
+ } else if (input instanceof IConstant) {
+ return ((IConstant) input).c().name();
} else if (input instanceof IBinFormula) {
return ((IBinFormula) input).j().toString();
} else if (input instanceof IFormulaITE || input instanceof ITermITE) {
