diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 9da720ccc..de3578fae 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -206,12 +206,12 @@ namespace Duality {
                                          0,
                                          0,
                                          num_pats,
-                                         &pats[0],
+                                         VEC2PTR(pats),
                                          num_no_pats,
-                                         &no_pats[0],
+                                         VEC2PTR(no_pats),
                                          bound,
-                                         &sorts[0],
-                                         &names[0],
+                                         VEC2PTR(sorts),
+                                         VEC2PTR(names),
                                          new_body);
         return expr(ctx,foo);
 #endif
@@ -244,7 +244,7 @@ namespace Duality {
                     res = HideVariable(t, e->number);
                 }
                 else {
-                    res = f(args.size(), &args[0]);
+                    res = f(args.size(), VEC2PTR(args));
                 }
             }
         }
@@ -354,7 +354,7 @@ namespace Duality {
             int nargs = t.num_args();
             for (int i = 0; i < nargs; i++)
                 args.push_back(SubstRec(memo, t.arg(i)));
-            res = f(args.size(), &args[0]);
+            res = f(args.size(), VEC2PTR(args));
         }
         else if (t.is_quantifier()) {
             std::vector<expr> pats;
@@ -384,7 +384,7 @@ namespace Duality {
             hash_map<func_decl, func_decl>::iterator it = map.find(f);
             if (it != map.end())
                 f = it->second;
-            res = f(args.size(), &args[0]);
+            res = f(args.size(), VEC2PTR(args));
         }
         else if (t.is_quantifier()) {
             std::vector<expr> pats;
@@ -411,7 +411,7 @@ namespace Duality {
             int nargs = t.num_args();
             for (int i = 0; i < nargs; i++)
                 args.push_back(ExtractStores(memo, t.arg(i), cnstrs, renaming));
-            res = f(args.size(), &args[0]);
+            res = f(args.size(), VEC2PTR(args));
             if (f.get_decl_kind() == Store) {
                 func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort());
                 expr y = fresh();
@@ -720,7 +720,7 @@ namespace Duality {
                         }
                 }
             }
-            res = f(args.size(), &args[0]);
+            res = f(args.size(), VEC2PTR(args));
         }
         else if (t.is_quantifier()) {
             Term body = IneqToEqRec(memo, t.body());
@@ -751,7 +751,7 @@ namespace Duality {
             }
             for (int i = 0; i < nargs; i++)
                 args.push_back(SubstRec(memo, t.arg(i)));
-            res = f(args.size(), &args[0]);
+            res = f(args.size(), VEC2PTR(args));
         }
         else if (t.is_quantifier())
             res = CloneQuantifier(t, SubstRec(memo, t.body()));
@@ -1064,7 +1064,7 @@ namespace Duality {
         if (core_size && core) {
             std::vector<expr> full_core(alit_stack.size()), core1(n);
             std::copy(assumptions, assumptions + n, core1.begin());
-            res = slvr().check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]);
+            res = slvr().check(alit_stack.size(), VEC2PTR(alit_stack), core_size, VEC2PTR(full_core));
             full_core.resize(*core_size);
             if (res == unsat) {
                 FilterCore(core1, full_core);
@@ -1073,7 +1073,7 @@ namespace Duality {
             }
         }
         else 
-            res = slvr().check(alit_stack.size(), &alit_stack[0]);
+            res = slvr().check(alit_stack.size(), VEC2PTR(alit_stack));
         alit_stack.resize(oldsiz);
         return res;
     }
@@ -1241,7 +1241,7 @@ namespace Duality {
     check_result RPFP_caching::CheckCore(const std::vector<Term> &assumps, std::vector<Term> &core){
         core.resize(assumps.size());
         unsigned core_size;
-        check_result res = slvr().check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]);
+        check_result res = slvr().check(assumps.size(),(expr *)VEC2PTR(assumps),&core_size, VEC2PTR(core));
         if(res == unsat)
             core.resize(core_size);
         else
@@ -1451,13 +1451,13 @@ namespace Duality {
             if (underapprox_core) {
                 std::vector<expr> unsat_core(us.size());
                 unsigned core_size = 0;
-                res = slvr_check(us.size(), &us[0], &core_size, &unsat_core[0]);
+                res = slvr_check(us.size(), VEC2PTR(us), &core_size, VEC2PTR(unsat_core));
                 underapprox_core->resize(core_size);
                 for (unsigned i = 0; i < core_size; i++)
                     (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]);
             }
             else {
-                res = slvr_check(us.size(), &us[0]);
+                res = slvr_check(us.size(), VEC2PTR(us));
                 bool dump = false;
                 if (dump) {
                     std::vector<expr> cnsts;
@@ -1477,7 +1477,7 @@ namespace Duality {
     check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){
         // check_result temp1 = slvr_check(); // no idea why I need to do this
         ClearProofCore();
-        check_result res = slvr_check(assumps.size(),&assumps[0]);
+        check_result res = slvr_check(assumps.size(), VEC2PTR(assumps));
         model mod = slvr().get_model();
         if(!mod.null())
             dualModel = mod;;
@@ -1939,7 +1939,7 @@ namespace Duality {
             else {
                 for (int i = 0; i < nargs; i++)
                     args.push_back(ResolveIte(memo, t.arg(i), lits, done, dont_cares));
-                res = f(args.size(), &args[0]);
+                res = f(args.size(), VEC2PTR(args));
             }
         }
         else res = t;
@@ -1975,7 +1975,7 @@ namespace Duality {
                 else {
                     for (int i = 0; i < nargs; i++)
                         args.push_back(ElimIteRec(memo, t.arg(i), cnsts));
-                    res = t.decl()(args.size(), &args[0]);
+                    res = t.decl()(args.size(), VEC2PTR(args));
                 }
             }
             else if (t.is_quantifier())
@@ -2762,14 +2762,14 @@ namespace Duality {
         }
     
         // verify
-        check_result res = s.check(lits.size(),&lits[0]);
+        check_result res = s.check(lits.size(), VEC2PTR(lits));
         if(res != unsat){
             // add the axioms in the off chance they are useful
             const std::vector<expr> &theory = ls->get_axioms();
             for(unsigned i = 0; i < theory.size(); i++)
                 s.add(theory[i]);
             for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
-                if(s.check(lits.size(),&lits[0]) == unsat)
+                if(s.check(lits.size(), VEC2PTR(lits)) == unsat)
                     goto is_unsat;
             throw "should be unsat";
         }
@@ -2777,7 +2777,7 @@ namespace Duality {
         for(unsigned i = 0; i < conjuncts.size(); ){
             std::swap(conjuncts[i],conjuncts.back());
             std::swap(lits[i],lits.back());
-            check_result res = s.check(lits.size()-1,&lits[0]);
+            check_result res = s.check(lits.size()-1, VEC2PTR(lits));
             if(res != unsat){
                 std::swap(conjuncts[i],conjuncts.back());
                 std::swap(lits[i],lits.back());
@@ -2801,7 +2801,7 @@ namespace Duality {
             lits.push_back(!b);
             expr bv = dualModel.eval(b);
             if(eq(bv,ctx.bool_val(true))){
-                check_result  res = slvr_check(lits.size(),&lits[0]);
+                check_result  res = slvr_check(lits.size(), VEC2PTR(lits));
                 if(res == unsat)
                     lits.pop_back();
                 else
@@ -2823,10 +2823,10 @@ namespace Duality {
             RedVars(negnodes[i], b, v);
             lits.push_back(!b);
         }
-        check_result res = slvr_check(lits.size(),&lits[0]);
+        check_result res = slvr_check(lits.size(), VEC2PTR(lits));
         if(res == unsat && posnodes.size()){
             lits.resize(posnodes.size());
-            res = slvr_check(lits.size(),&lits[0]);
+            res = slvr_check(lits.size(), VEC2PTR(lits));
         }
         dualModel = slvr().get_model();
 #if 0
@@ -3379,7 +3379,7 @@ namespace Duality {
         int nargs = t.num_args();
         for(int i = 0; i < nargs; i++)
             sorts.push_back(t.arg(i).get_sort());
-        return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort());
+        return ctx.function(name.c_str(), nargs, VEC2PTR(sorts), t.get_sort());
     }
 
     Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n)
@@ -3390,7 +3390,7 @@ namespace Duality {
         std::vector<sort> domain;
         for(int i = 0; i < arity; i++)
         domain.push_back(f.domain(i));
-        return ctx.function(name.c_str(), arity, &domain[0], f.range());
+        return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
     }
 
     Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n)
@@ -3401,7 +3401,7 @@ namespace Duality {
         std::vector<sort> domain;
         for(int i = 0; i < arity; i++)
         domain.push_back(f.domain(i));
-        return ctx.function(name.c_str(), arity, &domain[0], f.range());
+        return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
     }
 
     // Scan the clause body for occurrences of the predicate unknowns
@@ -3426,7 +3426,7 @@ namespace Duality {
             std::vector<Term> args;
             for(int i = 0; i < nargs; i++)
                 args.push_back(ScanBody(memo,t.arg(i),pmap,parms,nodes));
-            res = f(nargs,&args[0]);
+            res = f(nargs, VEC2PTR(args));
         }
         else if (t.is_quantifier())
             res = CloneQuantifier(t,ScanBody(memo,t.body(),pmap,parms,nodes));
@@ -3474,7 +3474,7 @@ namespace Duality {
                 std::vector<Term> args;
                 for(int i = 0; i < nargs; i++)
                     args.push_back(RemoveLabelsRec(memo,t.arg(i),lbls));
-                res = f(nargs,&args[0]);
+                res = f(nargs, VEC2PTR(args));
             }
         }
         else if (t.is_quantifier())
@@ -3505,7 +3505,7 @@ namespace Duality {
                     ls->declare_constant(f);  // keep track of background constants
                 for(int i = 0; i < nargs; i++)
                     args.push_back(SubstBoundRec(memo, subst, level, t.arg(i)));
-                res = f(args.size(),&args[0]);
+                res = f(args.size(), VEC2PTR(args));
             }
         else if (t.is_quantifier()){
             int bound = t.get_quantifier_num_bound();
@@ -3545,7 +3545,7 @@ namespace Duality {
                 int nargs = t.num_args();
                 for(int i = 0; i < nargs; i++)
                     args.push_back(DeleteBoundRec(memo, level, num, t.arg(i)));
-                res = f(args.size(),&args[0]);
+                res = f(args.size(), VEC2PTR(args));
             }
         else if (t.is_quantifier()){
             int bound = t.get_quantifier_num_bound();
@@ -3729,7 +3729,7 @@ namespace Duality {
                         Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
                 }
 #endif
-                Node *node = CreateNode(R(Indparams.size(),&Indparams[0]));
+                Node *node = CreateNode(R(Indparams.size(),VEC2PTR(Indparams)));
                 //nodes.push_back(node);
                 pmap[R] = node;
                 if (is_query)
@@ -4007,7 +4007,7 @@ namespace Duality {
                     std::vector<Term> args;
                     for(int k = 0; k < nargs; k++)
                         args.push_back(new_lit.arg(k));
-                    new_lit = fd(nargs,&args[0]);
+                    new_lit = fd(nargs, VEC2PTR(args));
                     in_edge->F.RelParams[j] = fd;
                     hash_map<ast,expr> map;
                     map[lit] = new_lit;
@@ -4201,10 +4201,10 @@ namespace Duality {
                 if(rit != e->relMap.end()){
                     Node* child = e->Children[rit->second];
                     FuncDecl op = child->Name;
-                    res = op(args.size(),&args[0]);
+                    res = op(args.size(), VEC2PTR(args));
                 }
                 else {
-                    res = f(args.size(),&args[0]);
+                    res = f(args.size(), VEC2PTR(args));
                     if(nargs == 0 && t.decl().get_decl_kind() == Uninterpreted)
                         quants.push_back(t);
                 }
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index d935c2655..b3a96aea4 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -3457,7 +3457,7 @@ namespace Duality {
                     arg_sorts.push_back(params[j].get_sort());
                 arg_sorts.push_back(ctx.int_sort());
                 std::string new_name = std::string("@db@") + node->Name.name().str();
-                func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), &arg_sorts[0],ctx.bool_sort());
+                func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), VEC2PTR(arg_sorts),ctx.bool_sort());
                 std::vector<expr> args = params;
                 args.push_back(dvar);
                 expr pat = f(args);
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 3b29adc41..7ee76d4d6 100755
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -120,7 +120,7 @@ namespace Duality {
             a.resize(args.size());
         for(unsigned i = 0; i < args.size(); i++)
             a[i] = to_expr(args[i].raw());
-        return make(op,args.size(), args.size() ? &a[0] : 0);
+        return make(op,args.size(), args.size() ? VEC2PTR(a) : 0);
     }
 
     expr context::make(decl_kind op){
@@ -165,11 +165,11 @@ namespace Duality {
             bound_asts.push_back(a);
         }
         expr_ref abs_body(m());
-        expr_abstract(m(), 0, num_bound, &bound_asts[0], to_expr(body.raw()), abs_body);
+        expr_abstract(m(), 0, num_bound, VEC2PTR(bound_asts), to_expr(body.raw()), abs_body);
         expr_ref result(m());
         result = m().mk_quantifier(
             op == Forall, 
-            names.size(), &types[0], &names[0], abs_body.get(),            
+            names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(),            
             0, 
             ::symbol(),
             ::symbol(),
@@ -195,7 +195,7 @@ namespace Duality {
         expr_ref result(m());
         result = m().mk_quantifier(
             op == Forall, 
-            names.size(), &types[0], &names[0], to_expr(body.raw()),            
+            names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()),            
             0, 
             ::symbol(),
             ::symbol(),
@@ -305,7 +305,7 @@ namespace Duality {
         std::vector< ::expr *> _args(n);
         for(unsigned i = 0; i < n; i++)
             _args[i] = to_expr(args[i].raw());
-        return ctx().cook(m().mk_app(to_func_decl(raw()),n,&_args[0]));
+        return ctx().cook(m().mk_app(to_func_decl(raw()),n,VEC2PTR(_args)));
     }
 
     int solver::get_num_decisions(){
@@ -377,7 +377,7 @@ namespace Duality {
         std::vector< ::expr *> _patterns(num_patterns);
         for(unsigned i = 0; i < num_patterns; i++)
             _patterns[i] = to_expr(patterns[i].raw());
-        return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw())));
+        return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, VEC2PTR(_patterns), to_expr(b.raw())));
     }
 
     expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
@@ -414,7 +414,7 @@ namespace Duality {
             _domain[i] = to_sort(domain[i].raw());
         ::func_decl* d = m().mk_fresh_func_decl(prefix, 
                                                 _domain.size(), 
-                                                &_domain[0],
+                                                VEC2PTR(_domain),
                                                 to_sort(range.raw()));
         return func_decl(*this,d);
     }
@@ -453,16 +453,15 @@ namespace Duality {
         lb = Z3_interpolate(
             ctx(),
             _assumptions.size(),
-            &_assumptions[0],
+            VEC2PTR(_assumptions),
             0,
             0,
-            &_interpolants[0],
+            VEC2PTR(_interpolants),
             &_model,
             &_labels,
             incremental,
             _theory.size(),
-            &_theory[0]
-                            );
+            VEC2PTR(_theory));
     
         if(lb == Z3_L_FALSE){
             interpolants.resize(_interpolants.size());
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index a84d8899c..b5027d7d2 100644
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -891,7 +891,7 @@ namespace Duality {
                 _assumptions[i] = to_expr(assumptions[i]);
             }
             the_model = 0;
-            lbool r = m_solver->check_sat(n,&_assumptions[0]);
+            lbool r = m_solver->check_sat(n, VEC2PTR(_assumptions));
 	  
             if(core_size && core){
                 ptr_vector< ::expr> _core;
@@ -1182,7 +1182,7 @@ namespace Duality {
         std::vector< ::sort *> sv(arity);
         for(unsigned i = 0; i < arity; i++)
             sv[i] = domain[i];
-        ::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range);
+        ::func_decl* d = m().mk_func_decl(name,arity, VEC2PTR(sv),range);
         return func_decl(*this,d);
     }
 
@@ -1227,7 +1227,7 @@ namespace Duality {
     inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
 
     inline expr func_decl::operator()(const std::vector<expr> &args) const {
-        return operator()(args.size(),&args[0]);
+        return operator()(args.size(), VEC2PTR(args));
     }
     inline expr func_decl::operator()() const {
         return operator()(0,0);
diff --git a/src/util/util.h b/src/util/util.h
index 1e15b526c..39fcb0122 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -59,6 +59,7 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8);
 #define SPRINTF sprintf
 #endif
 
+#define VEC2PTR(_x_) ((_x_).size() ? &(_x_)[0] : 0)
 
 #ifdef _WINDOWS
 // Disable thread local declspec as it seems to not work downlevel.