diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index e0bb04c10..b98e6b182 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -60,11 +60,11 @@ namespace sat {
 
     void card_extension::init_watch(card& c, bool is_true) {
         clear_watch(c);
-        if (c.lit().sign() == is_true) {
+        if (c.lit() != null_literal && c.lit().sign() == is_true) {
             c.negate();
         }
         TRACE("sat", display(tout << "init watch: ", c, true););
-        SASSERT(value(c.lit()) == l_true);
+        SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
         unsigned j = 0, sz = c.size(), bound = c.k();
         if (bound == sz) {
             for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
@@ -153,12 +153,12 @@ namespace sat {
             if (s().m_config.m_drat) {
                 svector<drat::premise> ps;
                 literal_vector lits;
-                lits.push_back(~c.lit());
+                if (c.lit() != null_literal) lits.push_back(~c.lit());
                 for (unsigned i = c.k(); i < c.size(); ++i) {
                     lits.push_back(c[i]);
                 }
                 lits.push_back(lit);
-                ps.push_back(drat::premise(drat::s_ext(), c.lit()));
+                ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case.
                 s().m_drat.add(lits, ps);
             }
             s().assign(lit, justification::mk_ext_justification(c.index()));
@@ -220,7 +220,7 @@ namespace sat {
 
     void card_extension::init_watch(xor& x, bool is_true) {
         clear_watch(x);
-        if (x.lit().sign() == is_true) {
+        if (x.lit() != null_literal && x.lit().sign() == is_true) {
             x.negate();
         }
         unsigned sz = x.size();
@@ -261,7 +261,7 @@ namespace sat {
             if (s().m_config.m_drat) {
                 svector<drat::premise> ps;
                 literal_vector lits;
-                lits.push_back(~x.lit());
+                if (x.lit() != null_literal) lits.push_back(~x.lit());
                 for (unsigned i = 1; i < x.size(); ++i) {
                     lits.push_back(x[i]);
                 }
@@ -302,7 +302,7 @@ namespace sat {
         TRACE("sat", tout << "assign: " << x.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";);
 
         SASSERT(value(alit) != l_undef);
-        SASSERT(value(x.lit()) == l_true);
+        SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
         unsigned index = 0;
         for (; index <= 2; ++index) {
             if (x[index].var() == alit.var()) break;
@@ -685,7 +685,7 @@ namespace sat {
     void card_extension::process_card(card& c, int offset) {
         literal lit = c.lit();
         SASSERT(c.k() <= c.size());       
-        SASSERT(value(lit) == l_true);
+        SASSERT(lit == null_literal || value(lit) == l_true);
         SASSERT(0 < offset);
         for (unsigned i = c.k(); i < c.size(); ++i) {
             process_antecedent(c[i], offset);
@@ -693,7 +693,9 @@ namespace sat {
         for (unsigned i = 0; i < c.k(); ++i) {
             inc_coeff(c[i], offset);                        
         }
-        process_antecedent(~lit, c.k() * offset);
+        if (lit != null_literal) {
+            process_antecedent(~lit, c.k() * offset);
+        }
     }
 
     void card_extension::process_antecedent(literal l, int offset) {
@@ -742,6 +744,7 @@ namespace sat {
         literal lit = v == null_bool_var ? null_literal : literal(v, false);
         card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
         m_cards.push_back(c);
+        std::cout << lit << "\n";
         if (v == null_bool_var) {
             // it is an axiom.
             init_watch(*c, true);
@@ -815,7 +818,7 @@ namespace sat {
                 }
                 else {
                     xor& x = index2xor(idx);
-                    if (lvl(x.lit()) > 0) r.push_back(x.lit());
+                    if (x.lit() != null_literal && lvl(x.lit()) > 0) r.push_back(x.lit());
                     if (x[1].var() == l.var()) {
                         x.swap(0, 1);
                     }
@@ -885,8 +888,8 @@ namespace sat {
                 }
                 SASSERT(found););
             
-            r.push_back(c.lit());
-            SASSERT(value(c.lit()) == l_true);
+            if (c.lit() != null_literal) r.push_back(c.lit());
+            SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
             for (unsigned i = c.k(); i < c.size(); ++i) {
                 SASSERT(value(c[i]) == l_false);
                 r.push_back(~c[i]);
@@ -894,9 +897,9 @@ namespace sat {
         }
         else {
             xor& x = index2xor(idx);
-            r.push_back(x.lit());
+            if (x.lit() != null_literal) r.push_back(x.lit());
             TRACE("sat", display(tout << l << " ", x, true););
-            SASSERT(value(x.lit()) == l_true);
+            SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
             SASSERT(x[0].var() == l.var() || x[1].var() == l.var());
             if (x[0].var() == l.var()) {
                 SASSERT(value(x[1]) != l_undef);
@@ -922,7 +925,7 @@ namespace sat {
 
         SASSERT(0 < bound && bound < sz);
         SASSERT(value(alit) == l_false);
-        SASSERT(value(c.lit()) == l_true);
+        SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
         unsigned index = 0;
         for (index = 0; index <= bound; ++index) {
             if (c[index] == alit) {
@@ -985,7 +988,7 @@ namespace sat {
             ptr_vector<card>::iterator it = begin, it2 = it, end = cards->end();
             for (; it != end; ++it) {
                 card& c = *(*it);
-                if (value(c.lit()) != l_true) {
+                if (c.lit() != null_literal && value(c.lit()) != l_true) {
                     continue;
                 }
                 switch (add_assign(c, ~l)) {
@@ -1028,7 +1031,7 @@ namespace sat {
             ptr_vector<xor>::iterator it = begin, it2 = it, end = xors->end();
             for (; it != end; ++it) {
                 xor& c = *(*it);
-                if (value(c.lit()) != l_true) {
+                if (c.lit() != null_literal && value(c.lit()) != l_true) {
                     continue;
                 }
                 switch (add_assign(c, ~l)) {
@@ -1101,7 +1104,8 @@ namespace sat {
             for (unsigned i = 0; i < c.size(); ++i) {
                 lits.push_back(c[i]);
             }
-            result->add_at_least(c.lit().var(), lits, c.k());
+            bool_var v = c.lit() == null_literal ? null_bool_var : c.lit().var();
+            result->add_at_least(v, lits, c.k());
         }
         for (unsigned i = 0; i < m_xors.size(); ++i) {
             literal_vector lits;
@@ -1109,7 +1113,8 @@ namespace sat {
             for (unsigned i = 0; i < x.size(); ++i) {
                 lits.push_back(x[i]);
             }
-            result->add_xor(x.lit().var(), lits);
+            bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
+            result->add_xor(v, lits);
         }
         return result;
     }
@@ -1285,7 +1290,7 @@ namespace sat {
         return !parity(x, 0);
     }
     bool card_extension::validate_unit_propagation(card const& c) { 
-        if (value(c.lit()) != l_true) return false;
+        if (c.lit() != null_literal && value(c.lit()) != l_true) return false;
         for (unsigned i = c.k(); i < c.size(); ++i) {
             if (value(c[i]) != l_false) return false;
         }
@@ -1353,7 +1358,7 @@ namespace sat {
                 for (unsigned i = 0; i < c.size(); ++i) {
                     p.push(c[i], offset);
                 }
-                p.push(~c.lit(), offset*c.k());
+                if (c.lit() != null_literal) p.push(~c.lit(), offset*c.k());
             }
             else {
                 literal_vector ls;
@@ -1362,7 +1367,8 @@ namespace sat {
                 for (unsigned i = 0; i < ls.size(); ++i) {
                     p.push(~ls[i], offset);
                 }
-                p.push(~index2xor(index).lit(), offset);
+                literal lxor = index2xor(index).lit();                
+                if (lxor != null_literal) p.push(~lxor, offset);
             }
             break;
         }
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index b58a1646c..979557d50 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -177,10 +177,6 @@ namespace sat {
 
     }
     
-    void local_search::display(std::ostream& out) {
-
-    }
-
     void local_search::add_clause(unsigned sz, literal const* c) {
         add_cardinality(sz, c, sz - 1);
     }
@@ -243,25 +239,38 @@ namespace sat {
                 unsigned n = c.size();
                 unsigned k = c.k();
 
-                // c.lit() <=> c.lits() >= k
-                // 
-                //    (c.lits() < k) or c.lit()
-                // =  (c.lits() + (n - k - 1)*~c.lit()) <= n    
-                //
-                //    ~c.lit() or (c.lits() >= k)
-                // =  ~c.lit() or (~c.lits() <= n - k)
-                // =  k*c.lit() + ~c.lits() <= n 
-                // 
 
-                lits.reset();
-                for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]);
-                for (unsigned j = 0; j < n - k - 1; ++j) lits.push_back(~c.lit());
-                add_cardinality(lits.size(), lits.c_ptr(), n);
-                
-                lits.reset();
-                for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]);
-                for (unsigned j = 0; j < k; ++j) lits.push_back(c.lit());
-                add_cardinality(lits.size(), lits.c_ptr(), n);
+
+                if (c.lit() == null_literal) {
+                    //    c.lits() >= k 
+                    // <=> 
+                    //    ~c.lits() <= n - k
+                    lits.reset();
+                    for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]);
+                    add_cardinality(lits.size(), lits.c_ptr(), n - k);
+                }
+                else {
+                    // TBD: this doesn't really work
+                    //
+                    // c.lit() <=> c.lits() >= k
+                    // 
+                    //    (c.lits() < k) or c.lit()
+                    // =  (c.lits() + (n - k - 1)*~c.lit()) <= n    
+                    //
+                    //    ~c.lit() or (c.lits() >= k)
+                    // =  ~c.lit() or (~c.lits() <= n - k)
+                    // =  k*c.lit() + ~c.lits() <= n 
+                    // 
+                    lits.reset();
+                    for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]);
+                    for (unsigned j = 0; j < n - k - 1; ++j) lits.push_back(~c.lit());
+                    add_cardinality(lits.size(), lits.c_ptr(), n);
+                    
+                    lits.reset();
+                    for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]);
+                    for (unsigned j = 0; j < k; ++j) lits.push_back(c.lit());
+                    add_cardinality(lits.size(), lits.c_ptr(), n);
+                }
             }
             //
             // xor constraints should be disabled.
@@ -277,83 +286,79 @@ namespace sat {
         ob_constraint.push_back(ob_term(v, weight));
     }
 
-    lbool local_search::check(parallel& p) {
-        flet<parallel*> _p(m_par, &p);
-        return check();
-    }
-
     lbool local_search::check() {
         return check(0, 0);
     }
     
-    lbool local_search::check(unsigned sz, literal const* assumptions) {
-        //sat_params params;
-        //std::cout << "my parameter value: " << params.cliff() << "\n";
+    lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) {
+        flet<parallel*> _p(m_par, p);
+        m_model.reset();
         unsigned num_constraints = m_constraints.size();
         for (unsigned i = 0; i < sz; ++i) {
             add_clause(1, assumptions + i);
         }
         init();
+        reinit();
         bool reach_known_best_value = false;
         bool_var flipvar;
         timer timer;
         timer.start();
-        bool reach_cutoff_time = false;
-        double elapsed_time;
         // ################## start ######################
+        IF_VERBOSE(1, verbose_stream() << "Unsat stack size: " << m_unsat_stack.size() << "\n";);
         //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
         //std::cout << num_vars() << '\n';
         unsigned tries, step = 0;
-        for (tries = 1; ; ++tries) {
+        for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) {
             reinit();
             for (step = 1; step <= max_steps; ++step) {
                 // feasible
                 if (m_unsat_stack.empty()) {
                     calculate_and_update_ob();
                     if (best_objective_value >= best_known_value) {
-                        reach_known_best_value = true;
                         break;
                     }
                 }
                 flipvar = pick_var();
                 flip(flipvar);
-                //std::cout << flipvar << '\t' << m_unsat_stack.size() << '\n';
-                //std::cout << goodvar_stack.size() << '\n';
 
                 m_vars[flipvar].m_time_stamp = step;
                 //if (!m_limit.inc()) break;pick_flip();
             }
-            //IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
+            IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
             // the following is for tesing
-            if (tries % 10 == 0) {
-                elapsed_time = timer.get_seconds();
-                //std::cout << tries << '\t' << elapsed_time << '\n';
-                if (elapsed_time > 300) {
-                    reach_cutoff_time = true;
-                    break;
-                }
-            }
+
             // tell the SAT solvers about the phase of variables.
             //if (m_par && tries % 10 == 0) {
                 //m_par->set_phase(*this);
-            if (reach_known_best_value || reach_cutoff_time) {
-                break;
-            }
         }
-        std::cout << elapsed_time << '\t' << reach_known_best_value << '\t' << reach_cutoff_time << '\t' << best_objective_value << '\n';
-        //IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " " << (reach_known_best_value ? "reached":"not reached") << "\n";);
 
         // remove unit clauses from assumptions.
         m_constraints.shrink(num_constraints);
         //print_solution();
-        IF_VERBOSE(1, verbose_stream() << (tries - 1) * max_steps + step << '\n';);
+        IF_VERBOSE(1, verbose_stream() << timer.get_seconds() <<  " steps: " << (tries - 1) * max_steps + step << " unsat stack: " << m_unsat_stack.size() << '\n';);
         if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true
+            extract_model();
             return l_true;
         }
         // TBD: adjust return status
         return l_undef;
     }
 
+
+    void local_search::sat(unsigned c) {
+        unsigned last_unsat_constraint = m_unsat_stack.back();
+        int index = m_index_in_unsat_stack[c];
+        m_unsat_stack[index] = last_unsat_constraint;
+        m_index_in_unsat_stack[last_unsat_constraint] = index;
+        m_unsat_stack.pop_back();
+    }
+
+    // swap the deleted one with the last one and pop
+    void local_search::unsat(unsigned c) {
+        m_index_in_unsat_stack[c] = m_unsat_stack.size();
+        m_unsat_stack.push_back(c);
+    }
+
     void local_search::flip(bool_var flipvar)
     {
         // already changed truth value!!!!
@@ -580,4 +585,46 @@ namespace sat {
             std::cout << v << "\t" << m_vars[v].m_neighbors.size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n';
         }
     }
+
+    void local_search::extract_model() {
+        m_model.reset();
+        for (unsigned v = 0; v < num_vars(); ++v) {
+            m_model.push_back(cur_solution[v] ? l_true : l_false);
+        }
+    }
+
+    void local_search::display(std::ostream& out) const {
+        for (unsigned i = 0; i < m_constraints.size(); ++i) {
+            constraint const& c = m_constraints[i];
+            display(out, c);
+        }
+    }
+    
+    void local_search::display(std::ostream& out, constraint const& c) const {
+        out << c.m_literals << " <= " << c.m_k << "\n";
+    }
+    
+    void local_search::display(std::ostream& out, unsigned v, var_info const& vi) const {
+        out << "v" << v << "\n";
+    }
+
+    bool local_search::check_goodvar() {
+        unsigned g = 0;
+        for (unsigned v = 0; v < num_vars(); ++v) {
+            if (conf_change(v) && score(v) > 0) {
+                ++g;
+                if (!already_in_goodvar_stack(v))
+                    std::cout << "3\n";
+            }
+        }
+        if (g == goodvar_stack.size())
+            return true;
+        else {
+            if (g < goodvar_stack.size())
+                std::cout << "1\n";
+            else
+                std::cout << "2\n"; // delete too many
+            return false;
+        }
+    }
 }
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index cba49e8ed..530e9a67b 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -151,6 +151,7 @@ namespace sat {
         reslimit    m_limit;
         random_gen  m_rand;
         parallel*   m_par;
+        model       m_model;
 
         void init();
         void reinit();
@@ -164,6 +165,10 @@ namespace sat {
 
         void flip(bool_var v);
 
+        void unsat(unsigned c);
+
+        void sat(unsigned c);
+
         bool tie_breaker_sat(bool_var v1, bool_var v2);
 
         bool tie_breaker_ccd(bool_var v1, bool_var v2);
@@ -174,48 +179,22 @@ namespace sat {
 
         void verify_solution();
 
-        void display(std::ostream& out);
-
         void print_info();
 
-        bool check_goodvar() {
-            unsigned g = 0;
-            for (unsigned v = 1; v <= num_vars(); ++v) {
-                if (conf_change(v) && score(v) > 0) {
-                    ++g;
-                    if (!already_in_goodvar_stack(v))
-                        std::cout << "3\n";
-                }
-            }
-            if (g == goodvar_stack.size())
-                return true;
-            else {
-                if (g < goodvar_stack.size())
-                    std::cout << "1\n";
-                else
-                    std::cout << "2\n"; // delete too many
-                return false;
-            }
-        }
+        void extract_model();
+
+        bool check_goodvar();
 
         void add_clause(unsigned sz, literal const* c);
 
+        void display(std::ostream& out) const;
 
-        void unsat(int c) {
-            m_index_in_unsat_stack[c] = m_unsat_stack.size();
-            m_unsat_stack.push_back(c);
-        }
-        // swap the deleted one with the last one and pop
-        void sat(int c) {
-            int last_unsat_constraint = m_unsat_stack.back();
-            int index = m_index_in_unsat_stack[c];
-            m_unsat_stack[index] = last_unsat_constraint;
-            m_index_in_unsat_stack[last_unsat_constraint] = index;
-            m_unsat_stack.pop_back();
-        }
+        void display(std::ostream& out, constraint const& c) const;
 
+        void display(std::ostream& out, unsigned v, var_info const& vi) const;
 
     public:
+
         local_search(solver& s);
 
         reslimit& rlimit() { return m_limit; }
@@ -228,9 +207,7 @@ namespace sat {
         
         lbool check();
 
-        lbool check(unsigned sz, literal const* assumptions);
-
-        lbool check(parallel& p);
+        lbool check(unsigned sz, literal const* assumptions, parallel* p = 0);
 
         local_search_config& config() { return m_config;  }
 
@@ -239,6 +216,8 @@ namespace sat {
         void set_phase(bool_var v, bool f) {}
 
         bool get_phase(bool_var v) const { return is_true(v); }
+
+        model& get_model() { return m_model; }
     };
 }
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index cf150217d..eea696547 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -782,10 +782,7 @@ namespace sat {
         pop_to_base_level();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(at_base_lvl());
-        if (m_config.m_local_search && !m_local_search) {
-            m_local_search = alloc(local_search, *this);
-        }
-        if ((m_config.m_num_threads > 1 || m_local_search) && !m_par) {
+        if ((m_config.m_num_threads > 1 || m_config.m_local_search) && !m_par) {
             return check_par(num_lits, lits);
         }
         flet<bool> _searching(m_searching, true);
@@ -866,8 +863,16 @@ namespace sat {
 
 
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
-        int num_threads = static_cast<int>(m_config.m_num_threads);
-        int num_extra_solvers = num_threads - 1 - (m_local_search ? 1 : 0);
+        bool use_local_search = m_config.m_local_search;
+        if (use_local_search) {
+            m_local_search = alloc(local_search, *this);
+        }
+
+        int num_threads = static_cast<int>(m_config.m_num_threads) + (use_local_search ? 1 : 0);
+        int num_extra_solvers = num_threads - 1 - (use_local_search ? 1 : 0);
+
+#define IS_LOCAL_SEARCH(i) i == num_extra_solvers && use_local_search
+
         sat::parallel par(*this);
         par.reserve(num_threads, 1 << 12);
         par.init_solvers(*this, num_extra_solvers);
@@ -881,12 +886,12 @@ namespace sat {
         for (int i = 0; i < num_threads; ++i) {
             try {                
                 lbool r = l_undef;
-                if (m_local_search && i == num_extra_solvers) {
-                    r = m_local_search->check(num_lits, lits);
-                }
-                else if (i < num_extra_solvers) {
+                if (i < num_extra_solvers) {
                     r = par.get_solver(i).check(num_lits, lits);
                 }
+                else if (IS_LOCAL_SEARCH(i)) {
+                    r = m_local_search->check(num_lits, lits);
+                }
                 else {
                     r = check(num_lits, lits);
                 }
@@ -897,6 +902,7 @@ namespace sat {
                         finished_id = i;
                         first = true;
                         result = r;
+                        std::cout << finished_id << " " << r << "\n";
                     }
                 }
                 if (first) {
@@ -908,7 +914,7 @@ namespace sat {
                             par.cancel_solver(j);
                         }
                     }
-                    if (i != num_extra_solvers) {
+                    if ((0 <= i && i < num_extra_solvers) || IS_LOCAL_SEARCH(i)) {
                         canceled = !rlimit().inc();
                         if (!canceled) {
                             rlimit().cancel();
@@ -936,10 +942,14 @@ namespace sat {
             m_core.reset();
             m_core.append(par.get_solver(finished_id).get_core());
         }
+        if (result == l_true && finished_id != -1 && IS_LOCAL_SEARCH(finished_id)) {
+            set_model(m_local_search->get_model());
+        }
         if (!canceled) {
             rlimit().reset_cancel();
         }
         set_par(0, 0);
+        m_local_search = 0;
         if (finished_id == -1) {
             switch (ex_kind) {
             case ERROR_EX: throw z3_error(error_code);
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 5e5625049..971843d55 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -424,15 +424,15 @@ struct goal2sat::imp {
         sat::literal_vector lits;
         unsigned sz = m_result_stack.size();
         convert_pb_args(t->get_num_args(), lits);
-        sat::bool_var v = m_solver.mk_var(true);
-        sat::literal lit(v, sign);
-        m_ext->add_at_least(v, lits, k.get_unsigned());
-        TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
         if (root) {
             m_result_stack.reset();
-            mk_clause(lit);
+            m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned());
         }
         else {
+            sat::bool_var v = m_solver.mk_var(true);
+            sat::literal lit(v, sign);
+            m_ext->add_at_least(v, lits, k.get_unsigned());
+            TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
             m_result_stack.shrink(sz - t->get_num_args());
             m_result_stack.push_back(lit);
         }
@@ -446,14 +446,14 @@ struct goal2sat::imp {
         for (unsigned i = 0; i < lits.size(); ++i) {
             lits[i].neg();
         }
-        sat::bool_var v = m_solver.mk_var(true);
-        sat::literal lit(v, sign);
-        m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
         if (root) {
             m_result_stack.reset();
-            mk_clause(lit);
+            m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned());
         }
         else {
+            sat::bool_var v = m_solver.mk_var(true);
+            sat::literal lit(v, sign);
+            m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
             m_result_stack.shrink(sz - t->get_num_args());
             m_result_stack.push_back(lit);
         }        
@@ -463,9 +463,8 @@ struct goal2sat::imp {
         SASSERT(k.is_unsigned());
         sat::literal_vector lits;
         convert_pb_args(t->get_num_args(), lits);
-        sat::bool_var v1 = m_solver.mk_var(true);
-        sat::bool_var v2 = m_solver.mk_var(true);
-        sat::literal l1(v1, false), l2(v2, false);
+        sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true);
+        sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true);
         m_ext->add_at_least(v1, lits, k.get_unsigned());        
         for (unsigned i = 0; i < lits.size(); ++i) {
             lits[i].neg();
@@ -473,16 +472,9 @@ struct goal2sat::imp {
         m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned());
         if (root) {
             m_result_stack.reset();
-            if (sign) {
-                mk_clause(~l1, ~l2);
-            }
-            else {
-                mk_clause(l1);
-                mk_clause(l2);
-            }
-            m_result_stack.reset();
         }
         else {
+            sat::literal l1(v1, false), l2(v2, false);
             sat::bool_var v = m_solver.mk_var();
             sat::literal l(v, false);
             mk_clause(~l, l1);
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 760fdcf54..c15680f72 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -186,7 +186,7 @@ class opb {
     app_ref parse_id() {
         bool negated = in.parse_token("~");
         if (!in.parse_token("x")) {
-            std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\")\n";
+            std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\" expected \"x\")\n";
             exit(3);
         }
         app_ref p(m);
@@ -228,10 +228,15 @@ class opb {
         return app_ref(m.mk_ite(e, c, arith.mk_numeral(rational(0), true)), m);
     }
 
-    void parse_objective() {
+    void parse_objective(bool is_min) {
         app_ref t = parse_term();
         while (!in.parse_token(";") && !in.eof()) {
-            t = arith.mk_add(t, parse_term());
+            if (is_min) {
+                t = arith.mk_add(t, parse_term());
+            }
+            else {
+                t = arith.mk_sub(t, parse_term());
+            }
         }
         g_handles.push_back(opt.add_objective(t, false));
     }
@@ -268,7 +273,10 @@ public:
                 in.skip_line();
             }
             else if (in.parse_token("min:")) {
-                parse_objective();
+                parse_objective(true);
+            }
+            else if (in.parse_token("max:")) {
+                parse_objective(false);
             }
             else {
                 parse_constraint();