fix String vs BigInteger in fp constr check

ultimate-pa · Sep 19, 2019 · b24bab0 · b24bab0
1 parent 78f498f
commit b24bab0
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java b/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java
@@ -991,8 +991,9 @@ public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final
 		defineFunction(new FunctionSymbolFactory("fp") {
 			@Override
 			public Sort getResultSort(final String[] indices, final Sort[] paramSorts, final Sort resultSort) {
+				final BigInteger fpSignIndex = toNumeral(paramSorts[0].getIndices()[0]);
 				if (indices != null || paramSorts.length != 3 || resultSort != null
-						|| paramSorts[0].getName() != "BitVec" || !paramSorts[0].getIndices()[0].equals(BigInteger.ONE)
+						|| paramSorts[0].getName() != "BitVec" || !fpSignIndex.equals(BigInteger.ONE)
 						|| paramSorts[1].getName() != "BitVec" || paramSorts[2].getName() != "BitVec") {
 					return null;
 				}