-added new tests

Author: DavidGalllob

src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java

@@ -1604,7 +1604,7 @@ && isInteger(operators.get(1))) {
           throw new ParserException(
               "fp.isZero requires exactly one " + "FloatingPointFormula operand.");
         }
-      case "fp.isInfinity":
+      case "fp.isInfinite":
         if (operands.size() == 1) {
           return Objects.requireNonNull(fpmgr).isInfinity((FloatingPointFormula) operands.get(0));
         } else {

src/org/sosy_lab/java_smt/test/SMTLIB2FloatingPointTest.java

@@ -351,6 +351,42 @@ public void testComplexFP()
     assertThat(proverEnvironment.isUnsat()).isFalse();
   }
 
+  @Test
+  public void testComplexFP2()
+      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
+    requireFloats();
+    assume().that(solverToUse()).isNotEqualTo(Solvers.BITWUZLA);
+    assume()
+        .withMessage("For some reason very slow here")
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.MATHSAT5);
+    String x =
+        "(declare-fun |c::main::$tmp::return_value_nondet_double$1@1!0&0#1|\n"
+            + "             ()\n"
+            + "             (_ FloatingPoint 11 53))\n"
+            + "(declare-fun |nondet$symex::nondet0| () (_ FloatingPoint 11 53))\n"
+            + "(declare-fun |c::main::main::1::x@1!0&0#1| () (_ FloatingPoint 11 53))\n"
+            + "(declare-fun |execution_statet::guard_exec@0!0| () Bool)\n"
+            + "(assert (= |nondet$symex::nondet0|\n"
+            + "   |c::main::$tmp::return_value_nondet_double$1@1!0&0#1|))\n"
+            + "(assert (= |c::main::$tmp::return_value_nondet_double$1@1!0&0#1|\n"
+            + "   |c::main::main::1::x@1!0&0#1|))\n"
+            + "(assert (let ((a!1 (not (=> true\n"
+            + "                    (=> |execution_statet::guard_exec@0!0|\n"
+            + "                        (fp.eq |c::main::main::1::x@1!0&0#1|\n"
+            + "                               |c::main::main::1::x@1!0&0#1|))))))\n"
+            + "  a!1))";
+
+    BooleanFormula parsed = mgr.universalParseFromString(x);
+    Generator.assembleConstraint(parsed);
+    System.out.println(parsed + "\n-----------\n");
+    System.out.println(Generator.getSMTLIB2String());
+    ProverEnvironment proverEnvironment = context.newProverEnvironment();
+    proverEnvironment.addConstraint(parsed);
+    assertThat(proverEnvironment.isUnsat()).isFalse();
+  }
+
+
   @Test
   public void testDeclareFloatingPointsWithBitVectors()
       throws IOException, SolverException, InterruptedException, InvalidConfigurationException {