diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh
new file mode 100644
index 000000000..959dccbbd
--- /dev/null
+++ b/scripts/vsts-mac.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+cd ..
+mkdir build
+CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py  --java --python
+cd build
+make
+make test-z3
+make cpp_example
+make c_example
+# make java_example
+# make python_example
+./cpp_example
+./test_capi
+
+git clone https://github.com/z3prover/z3test.git z3test
+ls
+python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2
\ No newline at end of file
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 4d2f39416..af4be915d 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -117,7 +117,7 @@ namespace opt {
         void maximize_objectives(expr_ref_vector& blockers);
         inf_eps const & saved_objective_value(unsigned obj_index);
         inf_eps current_objective_value(unsigned obj_index);
-        model* get_model(unsigned obj_index) { return m_models[obj_index]; }
+        model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; }
         bool objective_is_model_valid(unsigned obj_index) const {
             return m_valid_objectives[obj_index];
         }
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index f8f75fbfd..dd396126d 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -46,7 +46,7 @@ namespace opt {
         for (unsigned i = 0; i < src.size(); ++i) {
             if (src[i] >= dst[i]) {
                 dst[i] = src[i];
-                m_models.set(i, m_s->get_model(i));
+                m_models.set(i, m_s->get_model_idx(i));
                 m_s->get_labels(m_labels);
                 m_lower_fmls[i] = fmls[i].get();
                 if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.