Remove incomplete test (functionality already covered)

ftsrg · Oct 13, 2020 · 0050ab5 · 0050ab5
1 parent a31178c
commit 0050ab5
Showing 1 changed file with 0 additions and 11 deletions.
diff --git a/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java b/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java
@@ -420,17 +420,6 @@ public void testBV12() {
 		solver.pop();
 	}
 
-	public void testBV13() {
-		solver.push();
-
-		solver.add(BvExprs.Eq(uint16ToBvLitExpr(4), BvExprs.Add(List.of(uint16ToBvLitExpr(1), uint16ToBvLitExpr(3)))));
-		solver.add(BvExprs.Eq(uint16ToBvLitExpr(1), BvExprs.Sub(uint16ToBvLitExpr(4), uint16ToBvLitExpr(3))));
-		solver.add(BvExprs.Eq(uint16ToBvLitExpr(12), BvExprs.Mul(List.of(uint16ToBvLitExpr(3), uint16ToBvLitExpr(4)))));
-		solver.add(BvExprs.Eq(uint16ToBvLitExpr(4), BvExprs.SDiv(uint16ToBvLitExpr(12), uint16ToBvLitExpr(3))));
-		solver.add(BvExprs.Eq(uint16ToBvLitExpr(1), BvExprs.SMod(uint16ToBvLitExpr(13), uint16ToBvLitExpr(3))));
-		solver.add(BvExprs.Eq(uint16ToBvLitExpr(1), BvExprs.SRem(uint16ToBvLitExpr(13), uint16ToBvLitExpr(3))));
-	}
-
 	private static BvLitExpr uint16ToBvLitExpr(int value) {
 		return BvUtils.bigIntegerToUnsignedBvLitExpr(BigInteger.valueOf(value), 16);
 	}