From e0d46691166cc1450934bf606c3f79807e2c0589 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 Jul 2020 23:47:45 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bool_rewriter.cpp | 30 ++++++++++++++----------------
 1 file changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index da2584db7..d3dfe2812 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -136,7 +136,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
 
     unsigned sz = buffer.size();
 
-    switch(sz) {
+    switch (sz) {
     case 0:
         result = m().mk_true();
         return BR_DONE;
@@ -145,7 +145,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
         return BR_DONE;
     default:
         if (s) {
-            result = m().mk_and(sz, buffer.c_ptr());
+            result = m().mk_and(buffer);
             return BR_DONE;
         }
         return BR_FAILED;
@@ -166,16 +166,15 @@ br_status bool_rewriter::mk_flat_and_core(unsigned num_args, expr * const * args
             expr * arg = args[i];
             // Remark: all rewrites are depth 1.
             if (m().is_and(arg)) {
-                unsigned num = to_app(arg)->get_num_args();
-                for (unsigned j = 0; j < num; j++)
-                    flat_args.push_back(to_app(arg)->get_arg(j));
+                for (expr* e : *to_app(arg)) 
+                    flat_args.push_back(e);
             }
             else {
                 flat_args.push_back(arg);
             }
         }
         if (mk_nflat_and_core(flat_args.size(), flat_args.c_ptr(), result) == BR_FAILED)
-            result = m().mk_and(flat_args.size(), flat_args.c_ptr());
+            result = m().mk_and(flat_args);
         return BR_DONE;
     }
     return mk_nflat_and_core(num_args, args, result);
@@ -246,12 +245,12 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
         return BR_DONE;
     default:
         if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) {
-            if (local_ctx_simp(sz, buffer.c_ptr(), result))
+            if (local_ctx_simp(sz, buffer.c_ptr(), result)) 
                 return BR_DONE;
         }
         if (s) {
             ast_lt lt;
-            std::sort(buffer.begin(), buffer.end(), lt);
+            std::sort(buffer.begin(), buffer.end(), lt);       
             result = m().mk_or(sz, buffer.c_ptr());
             return BR_DONE;
         }
@@ -277,13 +276,12 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
             // Remark: all rewrites are depth 1.
             if (m().is_or(arg)) {
                 ordered = false;
-                unsigned num = to_app(arg)->get_num_args();
-                for (unsigned j = 0; j < num; j++)
-                    flat_args.push_back(to_app(arg)->get_arg(j));
+                for (expr* e : *to_app(arg)) 
+                    flat_args.push_back(e);
             }
             else {
                 flat_args.push_back(arg);
-                ordered &= !prev || !lt(arg, prev);
+                ordered &= (!prev || !lt(arg, prev));
                 prev = arg;
             }
         }
@@ -292,7 +290,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
                 ast_lt lt;
                 std::sort(flat_args.begin(), flat_args.end(), lt);
             }
-            result = m().mk_or(flat_args.size(), flat_args.c_ptr());
+            result = m().mk_or(flat_args);
         }
         return BR_DONE;
     }
@@ -342,7 +340,7 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
         new_args.push_back(arg);
     }
     if (simp) {
-        switch(new_args.size()) {
+        switch (new_args.size()) {
         case 0:
             result = m().mk_true();
             return true;
@@ -350,7 +348,7 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
             mk_not(new_args[0], result);
             return true;
         default:
-            result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr()));
+            result = m().mk_not(m().mk_or(new_args));
             return true;
         }
     }
@@ -796,7 +794,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
             for (unsigned j = i + 1; j < num_args; j++)
                 new_diseqs.push_back(m().mk_not(mk_eq(args[i], args[j])));
         }
-        result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr());
+        result = m().mk_and(new_diseqs);
         return BR_REWRITE3;
     }