Merge pull request #464 from sosy-lab/empty-sum-z3

Fix empty sums in Z3

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java

@@ -72,7 +72,11 @@ protected Long add(Long pNumber1, Long pNumber2) {
 
   @Override
   protected Long sumImpl(List<Long> operands) {
-    return Native.mkAdd(z3context, operands.size(), Longs.toArray(operands));
+    if (operands.isEmpty()) {
+      return makeNumberImpl(0);
+    } else {
+      return Native.mkAdd(z3context, operands.size(), Longs.toArray(operands));
+    }
   }
 
   @Override

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

@@ -69,6 +69,16 @@ public void distinctTest3() throws SolverException, InterruptedException {
     assertThatFormula(bmgr.and(imgr.distinct(symbols), bmgr.and(constraints))).isUnsatisfiable();
   }
 
+  @Test
+  public void trivialSumTest() throws SolverException, InterruptedException {
+    requireIntegers();
+    assertThatFormula(imgr.equal(imgr.sum(ImmutableList.of()), imgr.makeNumber(0)))
+        .isTautological();
+    assertThatFormula(
+            imgr.equal(imgr.sum(ImmutableList.of(imgr.makeVariable("a"))), imgr.makeVariable("a")))
+        .isTautological();
+  }
+
   @SuppressWarnings("CheckReturnValue")
   @Test
   public void failOnInvalidStringInteger() {