Skip to content

Commit ff72ddc

Browse files
committed
Ensure assume only throws upon predicate failure
1 parent f4a47f9 commit ff72ddc

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

src/java_bytecode/library/src/org/cprover/CProver.java

+2-3
Original file line numberDiff line numberDiff line change
@@ -117,10 +117,9 @@ public static <T> T nondetWithoutNull()
117117

118118
public static void assume(boolean condition)
119119
{
120-
if(enableAssume)
120+
if(enableAssume && !condition)
121121
{
122-
throw new RuntimeException(
123-
"Cannot execute program with CProver.assume()");
122+
throw new RuntimeException("CProver.assume() predicate is false");
124123
}
125124
}
126125
}

0 commit comments

Comments
 (0)