diff options
| author | Alasdair Armstrong | 2019-04-24 20:51:34 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-24 20:51:34 +0100 |
| commit | c6eb6b79daafb7dc44eb4e8a17409a1a04098ec6 (patch) | |
| tree | dc43770c447a365a034b3d7d3a392f7aa4b992a0 /src | |
| parent | ef237aea8d1667f1cbe13047acf1c916c94335e5 (diff) | |
SMT: Make sure we clear overflow checks between generating properties
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 44f32f4b..d48ecd9a 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -56,7 +56,7 @@ open Jib_util open Smtlib module IntMap = Map.Make(struct type t = int let compare = compare end) - + let zencode_upper_id id = Util.zencode_upper_string (string_of_id id) let zencode_id id = Util.zencode_string (string_of_id id) let zencode_name id = string_of_name ~deref_current_exception:false ~zencode:true id @@ -1481,8 +1481,9 @@ let smt_cdef props lets name_file ctx all_cdefs = function smt_header ctx stack all_cdefs; + Stack.clear overflow_checks; let ctx = { ctx with pragma_l = pragma_l; arg_stack = Stack.create () } in - + (* When we create each argument declaration, give it a unique location from the $property pragma, so we can identify it later. *) let arg_decls = |