[NLS] fix bug in circular definition of predicate's footprint and rea…

…chability
TDacik · Oct 10, 2024 · 585aa98 · 585aa98
1 parent d19054c
commit 585aa98
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/src/translation/predicate_encoding/NLS_Encodings.ml b/src/translation/predicate_encoding/NLS_Encodings.ml
@@ -51,12 +51,8 @@ module Default (Context : CONTEXT) = struct
       let types = Locations.mk_set_of_type ctx.locs top_path Sort.loc_nls in
 
       let loc = Variable.mk_fresh "loc" loc_sort in
-      let precond =
-        Boolean.mk_and [
-          Locations.mk_of_type ctx.locs loc Sort.loc_nls;
-          Set.mk_mem loc domain
-        ]
-      in
+      let precond = Set.mk_mem loc top_path in
+
       let bounds = nested_bounds.default :: nested_bounds.concrete in
       let i_bounds = Interval.meet_list bounds in
       let i_bounds = Interval.minus i_bounds (1, 1) in