rename symbol in test-case to avoid problems from repeated parsing.
OptiMathSAT5 throws an exception in a test,
because the renamed symbol was declared with different types (in different queries).
As re-declaring symbols is unspecified behaviour, lets change the test.
@@ -1058,14 +1058,14 @@ public class ModelTest extends SolverBasedTest0 {
"(declare-fun |f@2| () (_ FloatingPoint 8 23))"
+ "(declare-fun |p@3| () (_ BitVec 32))"
+ "(declare-fun *float@1 () (Array (_ BitVec 32) (_ FloatingPoint 8 23)))"
- + "(declare-fun |i@3| () (_ BitVec 32))"
+ + "(declare-fun |i@33| () (_ BitVec 32))"
+ "(declare-fun |Ai@| () (_ BitVec 32))"
+ "(declare-fun *unsigned_int@1 () (Array (_ BitVec 32) (_ BitVec 32)))"
+ "(assert (and (bvslt #x00000000 |Ai@|)"
+ " (bvslt #x00000000 (bvadd |Ai@| #x00000020))"
- + " (= |i@3| #x00000000)"
+ + " (= |i@33| #x00000000)"
+ " (= |p@3| |Ai@|)"
- + " (= (select *unsigned_int@1 |Ai@|) |i@3|)"
+ + " (= (select *unsigned_int@1 |Ai@|) |i@33|)"
+ " (= |f@2| (select *float@1 |p@3|))"
+ " (not (fp.eq ((_ to_fp 11 52) roundNearestTiesToEven |f@2|)"
+ " (_ +zero 11 52)))))";
