Skip to content

Commit

Permalink
Update crucible submodule to include GaloisInc/crucible#591.
Browse files Browse the repository at this point in the history
This fixes a previously-broken example in test_jvm_static_fields.
  • Loading branch information
Brian Huffman committed Jan 12, 2021
1 parent 01d3124 commit ee95fa1
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 5 deletions.
6 changes: 2 additions & 4 deletions intTests/test_jvm_static_fields/test.saw
Original file line number Diff line number Diff line change
Expand Up @@ -117,9 +117,7 @@ c_setY <-
}
z3;

// FIXME: this causes a translation error due to a bug in crucible-jvm
//c_getSum <-
fails (
c_getSum <-
jvm_verify c "getSum" [] false
do {
x <- jvm_fresh_var "x" java_long;
Expand All @@ -129,4 +127,4 @@ fails (
jvm_execute_func [];
jvm_return (jvm_term {{ x + y }});
}
z3);
z3;

0 comments on commit ee95fa1

Please sign in to comment.