Princess: Use variables to make the test for zero division more general

Author: daniel-raffler

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

@@ -208,6 +208,8 @@ public void testDivisionByZero() throws SolverException, InterruptedException {
 
     T a = nmgr.makeVariable("a");
     T b = nmgr.makeVariable("b");
+    T c = nmgr.makeVariable("c");
+
     T zero = nmgr.makeNumber(0);
 
     BooleanFormula f =
@@ -220,8 +222,9 @@ public void testDivisionByZero() throws SolverException, InterruptedException {
     // Division by zero is still a function. So, if (/0 a) = b and (/0 a) = c, then b=c must hold
     BooleanFormula g =
         bmgr.and(
-            nmgr.equal(nmgr.divide(a, zero), nmgr.makeNumber(2)),
-            nmgr.equal(nmgr.divide(a, zero), nmgr.makeNumber(4)));
+            nmgr.equal(nmgr.divide(a, zero), b),
+            nmgr.equal(nmgr.divide(a, zero), c),
+            bmgr.not(nmgr.equal(b, c)));
 
     assertThatFormula(g).isUnsatisfiable();
   }