Add test for #461

Author: daniel-raffler

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

@@ -26,6 +26,17 @@
 
 public class NumeralFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
+  @Test
+  public void mixedDivisionTest() throws SolverException, InterruptedException {
+    requireRationals();
+    assertThatFormula(
+            rmgr.equal(rmgr.divide(imgr.makeNumber(1), rmgr.makeNumber(2)), rmgr.makeNumber(0.5)))
+        .isTautological();
+    assertThatFormula(
+            rmgr.equal(rmgr.divide(rmgr.makeNumber(1), imgr.makeNumber(2)), rmgr.makeNumber(0.5)))
+        .isTautological();
+  }
+
   @Test
   public void distinctTest() throws SolverException, InterruptedException {
     requireIntegers();