diff --git a/src/duality/duality.h b/src/duality/duality.h
index 28cf96df3..e8f36a0cd 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -507,6 +507,7 @@ namespace Duality {
         {
             std::vector<Term> _IndParams;
             int nargs = t.num_args();
+            _IndParams.reserve(nargs);
             for(int i = 0; i < nargs; i++)
                 _IndParams.push_back(t.arg(i));
             Node *n = new Node(t.decl(),
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 9dae5eba9..b6dd42f00 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -234,6 +234,7 @@ namespace Duality {
             func_decl f = t.decl();
             std::vector<Term> args;
             int nargs = t.num_args();
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(LocalizeRec(e, memo, t.arg(i)));
             hash_map<func_decl, int>::iterator rit = e->relMap.find(f);
@@ -352,6 +353,7 @@ namespace Duality {
             func_decl f = t.decl();
             std::vector<Term> args;
             int nargs = t.num_args();
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(SubstRec(memo, t.arg(i)));
             res = f(args.size(), VEC2PTR(args));
@@ -379,6 +381,7 @@ namespace Duality {
             func_decl f = t.decl();
             std::vector<Term> args;
             int nargs = t.num_args();
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(SubstRec(memo, map, t.arg(i)));
             hash_map<func_decl, func_decl>::iterator it = map.find(f);
@@ -409,6 +412,7 @@ namespace Duality {
             func_decl f = t.decl();
             std::vector<Term> args;
             int nargs = t.num_args();
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(ExtractStores(memo, t.arg(i), cnstrs, renaming));
             res = f(args.size(), VEC2PTR(args));
@@ -655,6 +659,7 @@ namespace Duality {
             func_decl f = t.decl();
             std::vector<Term> args;
             int nargs = t.num_args();
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(RemoveRedundancyRec(memo, smemo, t.arg(i)));
 
@@ -703,6 +708,7 @@ namespace Duality {
             func_decl f = t.decl();
             std::vector<Term> args;
             int nargs = t.num_args();
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(IneqToEqRec(memo, t.arg(i)));
 
@@ -749,6 +755,7 @@ namespace Duality {
                 res = ctx.constant(name.c_str(), t.get_sort());
                 return res;
             }
+            args.reserve(nargs);
             for (int i = 0; i < nargs; i++)
                 args.push_back(SubstRec(memo, t.arg(i)));
             res = f(args.size(), VEC2PTR(args));
@@ -3308,6 +3315,7 @@ namespace Duality {
         std::string name = t.decl().name().str() + "_" + string_of_int(n);
         std::vector<sort> sorts;
         int nargs = t.num_args();
+        sorts.reserve(nargs);
         for(int i = 0; i < nargs; i++)
             sorts.push_back(t.arg(i).get_sort());
         return ctx.function(name.c_str(), nargs, VEC2PTR(sorts), t.get_sort());
@@ -3319,8 +3327,9 @@ namespace Duality {
         name = name.substr(0,name.rfind('_')) + "_" + string_of_int(n);
         int arity = f.arity();
         std::vector<sort> domain;
+        domain.reserve(arity);
         for(int i = 0; i < arity; i++)
-        domain.push_back(f.domain(i));
+            domain.push_back(f.domain(i));
         return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
     }
 
@@ -3330,8 +3339,9 @@ namespace Duality {
         name = name + "_" + string_of_int(n);
         int arity = f.arity();
         std::vector<sort> domain;
+        domain.reserve(arity);
         for(int i = 0; i < arity; i++)
-        domain.push_back(f.domain(i));
+            domain.push_back(f.domain(i));
         return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
     }
 
@@ -3355,6 +3365,7 @@ namespace Duality {
             }
             int nargs = t.num_args();
             std::vector<Term> args;
+            args.reserve(nargs);
             for(int i = 0; i < nargs; i++)
                 args.push_back(ScanBody(memo,t.arg(i),pmap,parms,nodes));
             res = f(nargs, VEC2PTR(args));
@@ -3403,6 +3414,7 @@ namespace Duality {
             else {
                 int nargs = t.num_args();
                 std::vector<Term> args;
+                args.reserve(nargs);
                 for(int i = 0; i < nargs; i++)
                     args.push_back(RemoveLabelsRec(memo,t.arg(i),lbls));
                 res = f(nargs, VEC2PTR(args));
@@ -3432,6 +3444,7 @@ namespace Duality {
                 func_decl f = t.decl();
                 std::vector<Term> args;
                 int nargs = t.num_args();
+                args.reserve(nargs);
                 if(nargs == 0 && f.get_decl_kind() == Uninterpreted)
                     ls->declare_constant(f);  // keep track of background constants
                 for(int i = 0; i < nargs; i++)
@@ -3474,6 +3487,7 @@ namespace Duality {
                 func_decl f = t.decl();
                 std::vector<Term> args;
                 int nargs = t.num_args();
+                args.reserve(nargs);
                 for(int i = 0; i < nargs; i++)
                     args.push_back(DeleteBoundRec(memo, level, num, t.arg(i)));
                 res = f(args.size(), VEC2PTR(args));
@@ -3870,6 +3884,7 @@ namespace Duality {
     void RPFP::AddParamsToNode(Node *node, const std::vector<expr> &params){
         int arity = node->Annotation.IndParams.size();
         std::vector<sort> domain;
+        domain.reserve(arity + params.size());
         for(int i = 0; i < arity; i++)
             domain.push_back(node->Annotation.IndParams[i].get_sort());
         for(unsigned i = 0; i < params.size(); i++)
@@ -3936,6 +3951,7 @@ namespace Duality {
                     func_decl fd = SuffixFuncDecl(new_lit,j);
                     int nargs = new_lit.num_args();
                     std::vector<Term> args;
+                    args.reserve(nargs);
                     for(int k = 0; k < nargs; k++)
                         args.push_back(new_lit.arg(k));
                     new_lit = fd(nargs, VEC2PTR(args));
@@ -4126,6 +4142,7 @@ namespace Duality {
                 // int idx;
                 std::vector<Term> args;
                 int nargs = t.num_args();
+                args.reserve(nargs);
                 for(int i = 0; i < nargs; i++)
                     args.push_back(ToRuleRec(e, memo, t.arg(i),quants));
                 hash_map<func_decl,int>::iterator rit = e->relMap.find(f);                 
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 59e68e046..6053295b5 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -3424,6 +3424,7 @@ namespace Duality {
                     func_decl f = t.decl();
                     std::vector<expr> args;
                     int nargs = t.num_args();
+                    args.reserve(nargs);
                     for(int i = 0; i < nargs; i++)
                         args.push_back(AddParamToRels(memo, rmap, p, t.arg(i)));
                     hash_map<func_decl,func_decl>::iterator rit = rmap.find(f);
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 6f918bccb..91b0c5a63 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -97,6 +97,7 @@ struct frame_reducer : public iz3mgr {
 
         // if multiple children of a tree node are used, we can't delete it
         std::vector<int> used_children; 
+        used_children.reserve(frames);
         for(int i = 0; i < frames; i++)
             used_children.push_back(0);
         for(int i = 0; i < frames; i++)
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 4831e7eaf..32b76b224 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1146,6 +1146,7 @@ public:
         my_cons.push_back(mk_not(farkas_con));
         my_coeffs.push_back(make_int("1"));
         std::vector<Iproof::node> my_hyps;
+        my_hyps.reserve(nargs);
         for(int i = 0; i < nargs; i++)
             my_hyps.push_back(iproof->make_hypothesis(my_cons[i]));
         ast res = iproof->make_farkas(mk_false(),my_hyps,my_cons,my_coeffs);
@@ -1203,6 +1204,7 @@ public:
         int nargs = num_prems(proof);
         if(nargs != (int)(my_coeffs.size()))
             throw "bad gomory-cut theory lemma";
+        my_prem_cons.reserve(nargs);
         for(int i = 0; i < nargs; i++)
             my_prem_cons.push_back(conc(prem(proof,i)));
         ast my_con = normalize_inequality(sum_inequalities(my_coeffs,my_prem_cons));
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 5ce4ef957..15f7f84d8 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -273,6 +273,7 @@ namespace Duality {
                     if (!heads.contains(fd)) {
                         int arity = f.arity();
                         std::vector<expr> args;
+                        args.reserve(arity);
                         for (int j = 0; j < arity; j++)
                             args.push_back(_d->ctx.fresh_func_decl("X", f.domain(j))());
                         expr c = implies(_d->ctx.bool_val(false), f(args));