Catch and ignore division by zero during cex reconstruction

osustarg · Sep 15, 2018 · 8affd22 · 8affd22
1 parent aee5e73
commit 8affd22
Showing 1 changed file with 13 additions and 8 deletions.
diff --git a/jkind/src/jkind/util/ModelReconstructionEvaluator.java b/jkind/src/jkind/util/ModelReconstructionEvaluator.java
@@ -66,15 +66,20 @@ private void reconstructValues(String property, int k) {
 		for (step = 0; step < k; step++) {
 			for (Dependency dependency : dependencies) {
 				if (dependency.type == DependencyType.VARIABLE) {
-					Value v1 = eval(new IdExpr(dependency.name));
-
-					// Compare computed value (v1) with solver value (v2)
-					if (!inlinedVariables.contains(dependency.name)) {
-						Value v2 = originalModel.getValue(new StreamIndex(dependency.name, step));
-						if (v2 != null && !v1.equals(v2)) {
-							throw new JKindException(
-									"Unable to reconstruct counterexample: variable value changed: " + dependency.name);
+					try {
+						Value v1 = eval(new IdExpr(dependency.name));
+
+						// Compare computed value (v1) with solver value (v2) when possible
+						if (!inlinedVariables.contains(dependency.name)) {
+							Value v2 = originalModel.getValue(new StreamIndex(dependency.name, step));
+							if (v2 != null && !v1.equals(v2)) {
+								throw new JKindException(
+										"Unable to reconstruct counterexample: variable value changed: "
+												+ dependency.name);
+							}
 						}
+					} catch (ArithmeticException ae) {
+						// Division by zero, ignore
 					}
 				}
 			}