From 5068d2083dc0609801f572a0e3d14df753d36a03 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 22 Apr 2017 11:36:03 -0700
Subject: [PATCH] tidy

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 15 ++++-----------
 src/smt/smt_context.h   |  2 +-
 2 files changed, 5 insertions(+), 12 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 32fb492ad..6a3c036ca 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3156,7 +3156,7 @@ namespace smt {
         setup_context(m_fparams.m_auto_config);
 
         expr_ref_vector theory_assumptions(m_manager);
-        get_theory_assumptions(theory_assumptions);
+        add_theory_assumptions(theory_assumptions);
         if (!theory_assumptions.empty()) {
             TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
             return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
@@ -3223,7 +3223,7 @@ namespace smt {
             (*it)->setup();
     }
 
-    void context::get_theory_assumptions(expr_ref_vector & theory_assumptions) {
+    void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
         ptr_vector<theory>::iterator it = m_theory_set.begin();
         ptr_vector<theory>::iterator end = m_theory_set.end();
         for (; it != end; ++it) {
@@ -3243,16 +3243,9 @@ namespace smt {
         if (!check_preamble(reset_cancel))
             return l_undef;
 
-        expr_ref_vector all_assumptions(m_manager);
-        for (unsigned i = 0; i < ext_num_assumptions; ++i) {
-            all_assumptions.push_back(ext_assumptions[i]);
-        }
+        expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
         if (!already_did_theory_assumptions) {
-            ptr_vector<theory>::iterator it = m_theory_set.begin();
-            ptr_vector<theory>::iterator end = m_theory_set.end();
-            for (; it != end; ++it) {
-                (*it)->add_theory_assumptions(all_assumptions);
-            }
+            add_theory_assumptions(all_assumptions);            
         }
 
         unsigned num_assumptions = all_assumptions.size();
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 4f0c14f5a..abdba86d1 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1059,7 +1059,7 @@ namespace smt {
 
         void reset_assumptions();
 
-        void get_theory_assumptions(expr_ref_vector & theory_assumptions);
+        void add_theory_assumptions(expr_ref_vector & theory_assumptions);
 
         lbool mk_unsat_core();