diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh
index a38ad86b2..522559b7c 100644
--- a/scripts/vsts-mac.sh
+++ b/scripts/vsts-mac.sh
@@ -5,6 +5,13 @@ 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
+./c_example
 
 
 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 92f66f4b6..f10be2291 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -2185,6 +2185,7 @@ namespace smt {
         unsigned idx = lits.size()-1;
         b_justification js;
         literal conseq = ~confl[2];
+        int bound = 1;
 
         while (m_num_marks > 0) {
 
@@ -2221,8 +2222,8 @@ namespace smt {
             //
             // Resolve selected conseq with antecedents.
             // 
-
-            int bound = 1;
+            
+            bound = 1;
 
             switch(js.get_kind()) {