wip - adding quasi macro detection

Z3Prover · Nov 30, 2022 · c1ff3d3 · c1ff3d3
1 parent 7b9dfb8
commit c1ff3d3
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp
@@ -135,7 +135,7 @@ bool eliminate_predicates::can_be_macro_head(expr* _head, unsigned num_bound) {
  * f(x,y,x+y+3,1) where x, y are the only bound variables
  */
 
-bool eliminate_predicates::can_be_quasi_macro_head(expr* head, unsigned num_bound) {
+bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bound) {
     if (!is_app(_head))
         return false;
     app* head = to_app(_head);
@@ -149,15 +149,15 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* head, unsigned num_boun
     uint_set indices;
     for (expr* arg : *head) {
         if (!is_var(arg))
-            return continue;
+            continue;
         unsigned idx = to_var(arg)->get_idx();
         if (indices.contains(idx))
-            return continue;
+            continue;
         if (idx >= num_bound)
             return false;
         indices.insert(idx);
     }
-    return indices.size() == num_bound;
+    return indices.num_elems() == num_bound;
 }