Princess: Add another case to the testDivisionByZero to check that (/ a 0) is still a function

(This part breaks if we use just `div` in Princess)

Author: daniel-raffler

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

@@ -216,6 +216,14 @@ public void testDivisionByZero() throws SolverException, InterruptedException {
             nmgr.equal(nmgr.divide(b, zero), nmgr.makeNumber(4)));
 
     assertThatFormula(f).isSatisfiable();
+
+    // 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)));
+
+    assertThatFormula(g).isUnsatisfiable();
   }
 
   @Test