diff --git a/fastsmt/cpp/goal_runner.cpp b/fastsmt/cpp/goal_runner.cpp
index 69ba99d..b620bc2 100644
--- a/fastsmt/cpp/goal_runner.cpp
+++ b/fastsmt/cpp/goal_runner.cpp
@@ -42,9 +42,9 @@ tactic fromString(context& ctx, std::string s) {
     return tactic(ctx, s.substr(7, (int)s.size() - 8).c_str());
   } else if (s.find("AndThen(") == 0) {
     auto tokens = split(s.substr(8, (int)s.size() - 9), ",");
-    
+
     tactic ret = fromString(ctx, tokens[0]);
-    
+
     for (size_t i = 1; i < tokens.size(); ++i) {
       auto tactic = fromString(ctx, tokens[i]);
       ret = ret & tactic;
@@ -79,7 +79,7 @@ tactic fromString(context& ctx, std::string s) {
 int get_rlimit(solver s) {
   auto stats = s.statistics();
   auto sz = stats.size();
-  
+
   for (size_t i = 0; i < sz; ++i) {
     if (stats.key(i) == "rlimit count") {
       return stats.uint_value(i);
@@ -91,25 +91,24 @@ int get_rlimit(solver s) {
 
 int main(int argc, char* argv[]) {
   context ctx;
-  
+
   char* strategy = argv[1];
   char* smt_input_file = argv[2];
   char* smt_out_file = argv[3];
-  
-  Z3_ast a = Z3_parse_smtlib2_file(ctx, smt_input_file, 0, 0, 0, 0, 0, 0);    
-  expr f(ctx, a);
 
-  tactic t = fromString(ctx, strategy);
+  try {
 
-  auto rlimit_before = get_rlimit(t.mk_solver());
+    // see https://github.com/Z3Prover/z3/issues/2798
+    expr f(ctx, mk_and(ctx.parse_file(smt_input_file)));
+    tactic t = fromString(ctx, strategy);
 
-  goal g(ctx);
-  g.add(f);
-  auto old_hash = g.as_expr().hash();
+    auto rlimit_before = get_rlimit(t.mk_solver());
 
-  clock_t begin = clock();
+    goal g(ctx);
+    g.add(f);
+    auto old_hash = g.as_expr().hash();
 
-  try {
+    clock_t begin = clock();
     apply_result r = t(g);
     assert(r.size() == 1); // assert that there is only 1 resulting goal
     goal new_goal = r[0];
@@ -145,7 +144,7 @@ int main(int argc, char* argv[]) {
     double elapsed_sec = (double)(end - begin) / CLOCKS_PER_SEC;
 
     std::cout << res << " " << rlimit << " " << old_hash << " " << new_hash << " " << elapsed_sec << std::endl;
-    
+
     std::vector<probe> probes;
     probes.push_back(probe(ctx, "num-consts"));
     probes.push_back(probe(ctx, "num-exprs"));
@@ -162,7 +161,7 @@ int main(int argc, char* argv[]) {
     probes.push_back(probe(ctx, "num-bv-consts"));
     probes.push_back(probe(ctx, "num-arith-consts"));
     probes.push_back(probe(ctx, "is-qfbv-eq"));
-  
+
     for (size_t i = 0; i < probes.size(); ++i) {
       if (i != 0) {
 	std::cout << " ";
@@ -174,6 +173,6 @@ int main(int argc, char* argv[]) {
     std::cout << -1 << std::endl;
     return 0;
   }
-  
+
   return 0;
 }
diff --git a/fastsmt/cpp/make_z3_4.6.2 b/fastsmt/cpp/make_z3_4.8.7
similarity index 100%
rename from fastsmt/cpp/make_z3_4.6.2
rename to fastsmt/cpp/make_z3_4.8.7
diff --git a/fastsmt/synthesis/search/models.py b/fastsmt/synthesis/search/models.py
index bb0cc1a..263cfc5 100644
--- a/fastsmt/synthesis/search/models.py
+++ b/fastsmt/synthesis/search/models.py
@@ -22,9 +22,9 @@
 import time
 
 try:
-    import fastText
+    import fasttext
 except ImportError:
-    logging.warn('fastText could not be imported (only needed to run fastText model).')
+    logging.warn('fasttext could not be imported (only needed to run fasttext model).')
 
 from abc import ABC, abstractmethod
 from sklearn.externals import joblib
@@ -136,7 +136,7 @@ def can_predict(self):
         return True
 
     def load_model(self, file):
-        self.bilinear_model = fastText.load_model(file + '.bin')
+        self.bilinear_model = fasttext.load_model(file + '.bin')
         print('Loaded bilinear model from ',file)
 
     def save_model(self, file):
@@ -187,7 +187,7 @@ def retrain(self):
 
         self.log.info('Created dataset of %d entries' % len(best_tactic))
 
-        self.bilinear_model = fastText.train_supervised(
+        self.bilinear_model = fasttext.train_supervised(
             input=train_file.name,
             epoch=self.config['models']['fast_text']['epoch'],
             lr=self.config['models']['fast_text']['lr'],
diff --git a/fastsmt/test/run_tests.sh b/fastsmt/test/run_tests.sh
index 992d837..c6389a1 100755
--- a/fastsmt/test/run_tests.sh
+++ b/fastsmt/test/run_tests.sh
@@ -1,3 +1,4 @@
+#!/bin/sh
 rm -f test/test_outcome.txt
 ./cpp/goal_runner "AndThen(With(simplify;blast_distinct=True;elim_and=False;flat=False;hoist_mul=False;local_ctx=True;pull_cheap_ite=True;push_ite_bv=True;som=True),Tactic(qfnra-nlsat),Tactic(sat),With(propagate-values;push_ite_bv=True),Tactic(max-bv-sharing),With(aig;aig_per_assertion=False),Tactic(smt))" test/bench_7150.smt2 test/out.smt2 | head -1 | awk '{ print $1 }' >> test/test_outcome.txt
 ./cpp/goal_runner "AndThen(With(simplify;blast_distinct=True;elim_and=False;flat=False;hoist_mul=True;local_ctx=False;pull_cheap_ite=True;push_ite_bv=True;som=True),Tactic(purify-arith),With(aig;aig_per_assertion=False),Tactic(elim-uncnstr),Tactic(smt))" test/bench_9849.smt2 test/out.smt2 | head -1 | awk '{ print $1 }' >> test/test_outcome.txt