Merge pull request kind2-mc#1051 from daniel-larraz/nested-quantifiers

Fix compilation of property with nested quantifiers
daniel-larraz · Feb 16, 2024 · 2396ac1 · 2396ac1
2 parents 80c00d2 + 0005dc0
commit 2396ac1
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml
@@ -787,9 +787,10 @@ and compile_ast_expr
     let bounds = bounds @
       List.map (fun v -> E.Unbound (E.unsafe_expr_of_term (Term.mk_var v)))
         vars in
-    H.add_seq !map.quant_vars (H.to_seq quant_var_map);
+    let quant_vars = H.to_seq quant_var_map in
+    H.add_seq !map.quant_vars quant_vars;
     let result = compile_unary bounds (mk vars) expr in
-    H.clear !map.quant_vars;
+    Seq.iter (fun (id, _) -> H.remove !map.quant_vars id) quant_vars;
     result
 
   and compile_equality bounds polarity expr1 expr2 =

diff --git a/tests/regression/success/nested_quantifiers.lus b/tests/regression/success/nested_quantifiers.lus
@@ -0,0 +1,5 @@
+
+node P() returns ();
+let
+  check forall (k1: int) ((exists (k2:int) k1=k2*k2) => k1>=0);
+tel