diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 5ff408bb7..afb7d25c4 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -302,6 +302,11 @@ extern "C" {
             parse_wcnf(*to_optimize_ptr(opt), s, h);
             return;
         }
+        if (ext && std::string("lp") == ext) {
+            unsigned_vector h;
+            parse_lp(*to_optimize_ptr(opt), s, h);
+            return;
+        }
         scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
         install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
         ctx->set_ignore_check(true);
diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp
index 9ac0f77a0..5ca1faed6 100644
--- a/src/opt/opt_parse.cpp
+++ b/src/opt/opt_parse.cpp
@@ -310,41 +310,164 @@ void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h) {
     opb.parse();
 }
 
-#if 0
+/**
+ * \brief Parser for a modest subset of the CPLEX LP format.
+ * Reference: http://eaton.math.rpi.edu/cplex90html/reffileformatscplex/reffileformatscplex5.html
+ */
 
-class lp_stream_buffer : opt_stream_buffer {
-public:    
-    lp_stream_buffer(std::istream & s):
-        opt_stream_buffer(s)
-    {}
-
-    char lower(char c) {
-        return ('A' <= c && c <= 'Z') ? c - 'A' + 'a' : c;
-    }
-
-    bool parse_token_nocase(char const* token) {
-        skip_whitespace();
-        char const* t = token;
-        while (lower(ch()) == *t) {
-            next();
-            ++t;
-        }
-        return 0 == *t;
-    }
+struct asymbol {
+    bool     m_is_num;
+    symbol   m_sym;
+    rational m_num;
+    unsigned m_line;
+    asymbol(symbol const& s, unsigned l): m_is_num(false), m_sym(s), m_line(l) {}
+    asymbol(rational const& r, unsigned l): m_is_num(true), m_num(r), m_line(l) {}
 };
 
-
 class lp_tokenizer {
-    opt_stream_buffer& in;
+    vector<asymbol>    m_tokens;
+    unsigned           m_pos;
+    svector<char>      m_buffer;
 public:
     lp_tokenizer(opt_stream_buffer& in):
-        in(in)
-    {}
+        m_pos(0)
+    {
+        parse_all(in);
+    }
+
+    symbol const& peek(unsigned i) {
+        if (i + m_pos >= m_tokens.size()) {
+            return symbol::null;
+        }
+        return m_tokens[i + m_pos].m_sym;
+    }
+
+    bool peek_num(unsigned i) {
+        if (i + m_pos >= m_tokens.size()) {
+            return false;
+        }
+        return m_tokens[i + m_pos].m_is_num;        
+    }
+
+    rational const& get_num(unsigned i) {
+        return m_tokens[i + m_pos].m_num;
+    }
+
+    void next(unsigned delta = 1) {
+        m_pos += delta;
+    }
+
+    bool eof() const {
+        return m_pos == m_tokens.size();
+    }
+
+    unsigned line() const {
+        if (m_pos < m_tokens.size()) return m_tokens[m_pos].m_line;
+        return 0;
+    }
+
+private:
+
+    bool is_separator(char c) {
+        return c == '\n' || c == '\\' || c == '*' || c == '+'; 
+    }
+
+    char lower(char c) {
+        if ('A' <= c && c <= 'Z')
+            return c - ('A' - 'a');
+        return c;
+    }
+
+    void parse_all(opt_stream_buffer& in) {
+        while (!in.eof()) {
+            in.skip_whitespace();
+            char c = in.ch();  
+            if (c == '\\') {
+                in.skip_line();
+                continue;
+            }
+
+            if (is_num(c)) {
+                rational n(0);
+                unsigned div = 1;
+                while (is_num(c) && !in.eof()) {
+                    n = n*rational(10) + rational(c - '0');
+                    in.next();
+                    c = in.ch();
+                }
+                if (c == '.') {
+                    in.next();
+                    while (is_num(c) && !in.eof()) {
+                        n = n*rational(10) + rational(c - '0');
+                        in.next();
+                        div *= 10;
+                        c = in.ch();
+                    }
+                }
+                if (div > 1) n = n / rational(div);
+                m_tokens.push_back(asymbol(n, in.line()));
+                continue;
+            }
+            m_buffer.reset();
+            if (is_alpha(c)) {
+                while (is_sym(c) && !in.eof()) {
+                    m_buffer.push_back(lower(c));
+                    in.next();
+                    c = in.ch();
+                }
+            }
+            else {
+                while (!is_ws(c) && !in.eof()) {
+                    m_buffer.push_back(c);
+                    in.next();
+                    c = in.ch();
+                }
+            }
+            m_buffer.push_back(0);
+            m_tokens.push_back(asymbol(symbol(m_buffer.c_ptr()), in.line()));
+        }
+    }
+
+    bool is_alpha(char c) const {
+        return ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z');
+    }
+
+    bool is_num(char c) const {
+        return '0' <= c && c <= '9';
+    }
+
+    bool is_ws(char c) const {
+        return c == ' ' || c == '\n' || c == '\t';
+    }
+
+    bool is_sym(char c) const {
+        return 
+            is_alpha(c) || 
+            is_num(c) ||
+            c == '!' ||
+            c == '"' ||
+            c == '#' ||
+            c == '$' ||
+            c == '%' ||
+            c == '&' ||
+            c == '{' ||
+            c == '}' ||
+            c == ',' ||
+            c == '.' ||
+            c == ';' ||
+            c == '?' ||
+            c == '@' ||
+            c == '`' ||
+            c == '\'' ||
+            c == '(' ||
+            c == ')' ||
+            c == '~';
+    }
     
 };
 
 class lp_parse {
-    typedef svector<std::pair<int, symbol> > lin_term;
+    typedef vector<std::pair<rational, symbol> > lin_term;
 
     struct objective {
         bool      m_is_max;
@@ -356,47 +479,96 @@ class lp_parse {
         le, ge, eq
     };
 
-    struct indicator {
-        symbol m_var;
-        bool   m_true;
-    };
-
     struct constraint {
-        optional<indicator> m_ind;
+        symbol   m_name;
+        symbol   m_bvar;
+        rational m_bval;
         lin_term m_expr;
         rel_op   m_rel;
-        int      m_bound;
+        rational m_bound;
+        constraint(symbol const& name, symbol const& v, rational const& val, lin_term& terms, rel_op r, rational const& bound):
+            m_name(name), m_bvar(v), m_bval(val), m_expr(terms), m_rel(r), m_bound(bound) {}
     };
 
     struct bound {
-        symbol            m_var;
-        option<rational>  m_lo, m_hi;
+        optional<rational>  m_lo, m_hi;
+        bool m_int;
+        bound() : m_int(false) {}
     };
 
-    opt::context&        opt;
-    lp_tokenizer&        tok;
-    objective            m_objective;
-    vector<constraint>   m_constraints;
-    vector<bound>        m_bounds;
-    hashtable<symbol, symbol_hash_proc, symbol_eq_proc> m_binary;
+    opt::context&       opt;
+    unsigned_vector&    m_h;
+    lp_tokenizer        tok;
+    objective           m_objective;
+    vector<constraint>  m_constraints;
+    map<symbol, bound, symbol_hash_proc, symbol_eq_proc> m_bounds;
 
 public:
 
-    lp_parse(opt::context& opt, lp_stream_buffer& in): 
-        opt(opt), tok(is) {}
+    lp_parse(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h) : 
+        opt(opt), m_h(h), tok(in) {}
     
     void parse() {
         parse_objective();
-        parse_subject_to();
-        parse_bounds();
-        parse_general();
-        parse_binary();
+        if (!try_subject_to()) {
+            error("subject to section expected");
+            return;
+        }
+         
+        while (!is_section()) {
+            parse_constraint();
+        }
+
+        while (true) {
+            if (is_bounds()) {
+                tok.next();
+                while (!is_section()) {
+                    parse_bound();
+                }
+            }
+            else if (is_binary()) {
+                tok.next();
+                while (!is_section()) {
+                    parse_binary();
+                }
+            }
+            else if (is_general()) {
+                tok.next();
+                while (!is_section()) {
+                    parse_general();
+                }
+            }
+            else {
+                break;
+            }
+        }
         post_process();
     }
 
+private:
+
+    void error(char const* msg) {
+        std::ostringstream ous;
+        ous << tok.line() << ": " << msg << " got: " << peek(0) << "\n";
+        throw default_exception(ous.str());
+    }
+        
+    symbol const& peek(unsigned i) { return tok.peek(i); }
+
+    bool try_accept(char * token) {
+        if (peek(0) == token) {
+            tok.next();
+            return true;
+        }
+        return false;
+    }
+
     void parse_objective() {
         m_objective.m_is_max = minmax();
-        m_objective.m_name = try_name();
+        if (peek(1) == ":") {
+            m_objective.m_name = peek(0);
+            tok.next(2);
+        }
         parse_expr(m_objective.m_expr);
     }
 
@@ -413,132 +585,218 @@ public:
         return false;
     }
 
+    void parse_constraint() {
+        symbol name;
+        if (peek(1) == ":") {
+            name = peek(0);
+            tok.next(2);
+        }
+        rational val(0);
+        symbol var;
+        parse_indicator(var, val);
+        lin_term terms;
+        parse_expr(terms);
+        rel_op op = parse_relation();
+        rational rhs = tok.get_num(0);
+        tok.next();
+        m_constraints.push_back(constraint(name, var, val, terms, op, rhs));
+    }
 
-    bool try_accept(char const* token) {
+    void parse_expr(lin_term& terms) {
+        bool pos = true;
+        if (peek(0) == "-") {
+            pos = false;
+            tok.next();
+        }
+        while (peek(0) == "+") {
+            tok.next();
+        }
+        terms.push_back(parse_term());
+        if (!pos) terms.back().first = -terms.back().first; 
+        while (peek(0) == "+" || peek(0) == "-") {
+            bool pos = peek(0) == "+";
+            tok.next();
+            terms.push_back(parse_term());
+            if (!pos) terms.back().first = -terms.back().first; 
+        }
+    }
+    
+    std::pair<rational, symbol> parse_term() {
+        std::pair<rational, symbol> r(rational::one(), peek(0));
+        if (tok.peek_num(0)) {
+            r.first = tok.get_num(0);
+            r.second = peek(1);
+            tok.next(2);
+        }
+        else {
+            tok.next(1);
+        }
+        return r;
+    }
+
+    rel_op parse_relation() {
+        if (try_accept("<=")) return le;
+        if (try_accept("=<")) return le;
+        if (try_accept(">=")) return ge;
+        if (try_accept("=>")) return ge;
+        if (try_accept("=")) return eq;
+        error("expected relation");
+        return eq;
+    }
+
+    bool peek_le(unsigned pos) {
+        return peek(pos) == "<=" || peek(pos) == "=<";
+    }
+
+    void parse_indicator(symbol& var, rational& val) {
+        if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
+            var = peek(0);
+            val = tok.get_num(2);
+            tok.next(4);
+        }
+    }
+
+    bool try_subject_to() {
+        if (try_accept("subject") && try_accept("to")) return true;
+        if (try_accept("such") && try_accept("that")) return true;
+        if (try_accept("st")) return true;
+        if (try_accept("s.t.")) return true;
         return false;
     }
 
-    bool parse_indicator(symbol& var, bool& val) {
-        if (!peek("=", 1)) return false;
-        if (!peek(":", 3)) return false;
-        if (!peek("1", 2) && !peek("0", 2)) return false;
-        val = peek("1",2);
-        parse_variable(var);
-        accept("=");
-        accept();
-        accept(":");
-        return true;
+    bool is_section() { return is_general() || is_binary() || is_bounds() || is_end();}
+    bool is_bounds() { return peek(0) == "bounds"; }
+    bool is_general() { return peek(0) == "general" || peek(0) == "gen" || peek(0) == "generals"; }
+    bool is_binary() { return peek(0) == "binary" || peek(0) == "binaries" || peek(0) == "bin"; }
+    bool is_end() { return peek(0) == "end" || tok.eof(); }
+
+    // lo <= x
+    // x <= hi
+    // lo <= x <= hi
+    // 
+    void parse_bound() {
+        symbol v;
+        if (peek_le(1) && tok.peek_num(0)) {
+            rational lhs = tok.get_num(0);
+            v = peek(2);
+            update_lower(lhs, v);
+            tok.next(3);
+            if (peek_le(0) && tok.peek_num(1)) {
+                rational rhs = tok.get_num(1);
+                update_upper(v, rhs);
+                tok.next(2);
+            }
+        }
+        if (peek_le(1) && tok.peek_num(2)) {
+            v = peek(0);
+            tok.next(2);
+            rational rhs = tok.get_num(0);
+            update_upper(v, rhs);
+            tok.next(1);
+        }
     }
 
-    void parse_bounds() {
-        if (!try_accept("bounds")) return;
-        
+    void update_lower(rational const& r, symbol const& v) {
+        bound b;
+        m_bounds.find(v, b);
+        b.m_lo = r;
+        m_bounds.insert(v, b);
     }
 
-    void parse_indicator() {
-
+    void update_upper(symbol const& v, rational const& r) {
+        bound b;
+        if (!m_bounds.find(v, b)) {
+            // set the lower bound to default 0
+            b.m_lo = rational::zero();
+        }
+        b.m_hi = r;
+        m_bounds.insert(v, b);
     }
-                
-    def indicator(self):
-        v = self.variable()
-        self.accept("=")
-        val = self.try_accept("1")
-        if val is None:
-            val = self.accept("0")            
-        self.accept("->")
-        return (var, val)
 
-    def try_indicator(self):
-        try:
-            return self.indicator()
-        with:
-            return None
+    void parse_binary() {
+        symbol const& v = peek(0);
+        update_lower(rational::zero(), v);
+        update_upper(v, rational::one());
+        m_bounds[v].m_int = true;
+        tok.next();
+    }
 
-    def constraints(self):
-        return [c for c in self._constraints()]
+    void parse_general() {
+        symbol const& v = peek(0);        
+        bound b;
+        m_bounds.find(v, b);        
+        b.m_int = true;
+        m_bounds.insert(v, b);
+        tok.next();        
+    }
     
-    def _constraints(self):
-        while True:
-            c = self.try_constraint()
-            if c in None:
-                return
-            yield c
+    void post_process() {
+        ast_manager& m = opt.get_manager();
+        arith_util a(m);
+        for (constraint const& c : m_constraints) {            
+            expr_ref fml(m);
+            expr_ref term = process_terms(c.m_expr);
+            bool is_int = a.is_int(term) && c.m_bound.is_int();
+            switch (c.m_rel) {
+            case le: fml = a.mk_le(term, a.mk_numeral(c.m_bound, is_int)); break;
+            case ge: fml = a.mk_ge(term, a.mk_numeral(c.m_bound, is_int)); break;
+            case eq: fml = m.mk_eq(term, a.mk_numeral(c.m_bound, is_int)); break;
+            }
+            if (c.m_bvar != symbol::null) {
+                term = mk_var(c.m_bvar);
+                bool is_int = c.m_bval.is_int() && a.is_int(term);
+                term = m.mk_eq(mk_var(c.m_bvar), a.mk_numeral(c.m_bval, is_int));
+                fml = m.mk_implies(term, fml);
+            }
+            opt.add_hard_constraint(fml);
+        }
+        for (auto const& kv : m_bounds) {
+            bound const& b = kv.m_value;
+            expr_ref term = mk_var(kv.m_key);
+            if (b.m_lo) {                
+                bool is_int = b.m_lo->is_int() && a.is_int(term);
+                opt.add_hard_constraint(a.mk_le(a.mk_numeral(*b.m_lo, is_int), term));
+            }
+            if (b.m_hi) {
+                bool is_int = b.m_hi->is_int() && a.is_int(term);
+                opt.add_hard_constraint(a.mk_le(term, a.mk_numeral(*b.m_hi, is_int)));
+            }
+        }
+        expr_ref term = process_terms(m_objective.m_expr);
+        m_h.push_back(opt.add_objective(to_app(term), m_objective.m_is_max));
+    }
 
-    def try_constraint(self):
-        try:
-            return self.constraint()
-        except:
-            return None
-        
-    def constraint(self):
-        name = self.try_label()
-        guard = self.try_guard()
-        e = self.expr()
-        op = self.relation()
-        rhs = self.numeral()
-        return (name, guard, e, ops, rhs)
+    expr_ref process_terms(lin_term const& terms) {
+        ast_manager& m = opt.get_manager();
+        arith_util a(m);
+        expr_ref_vector result(m);
+        for (auto const& kv : terms) {
+            expr_ref term = mk_var(kv.second);
+            if (!kv.first.is_one()) {
+                bool is_int = kv.first.is_int() && a.is_int(term);
+                term = a.mk_mul(a.mk_numeral(kv.first, is_int), term);
+            }
+            result.push_back(term);
+        }
+        return expr_ref(a.mk_add(result.size(), result.c_ptr()), m);
+    }
 
-    def expr(self):
-        return [t for t in self.terms()]
-
-    def terms(self):
-        while True:
-            t = self.term()
-            if t is None:
-                return None
-            yield t
-
-    def term(self):
-        sign = self.sign()
-        coeff = self.coeff()
-        v = self.variable()
-        return (sign*coeff, v)
-
-    def sign(self):
-        if self.try_accept("-"):
-            return -1
-        return 1
-
-    def coeff(self):
-        tok = self.peek()
-        if tok is int:
-            self.next()
-            return (int) tok
-        return 1
-
-    def relation(self):
-        if self.try_accept("<="):
-            return "<="
-        if self.try_accept(">="):
-            return ">="
-        if self.try_accept("=<"):
-            return "<="
-        if self.try_accept("=>"):
-            return ">="
-        if self.try_accept("="):
-            return "="
-        return None
-
-    def subject_to(self):
-        if self.accept("subject") and self.accept("to"):
-            return
-        if self.accept("such") and self.accept("that"):
-            return
-        if self.accept("st"):
-            return
-        if self.accept("s"):
-            self.try_accept(".")
-            self.accept("t")
-            self.accept(".")
-            return
-        
+    expr_ref mk_var(symbol const& v) {
+        ast_manager& m = opt.get_manager();
+        arith_util a(m);
+        bound b;
+        if (!m_bounds.find(v, b)) {
+            b.m_lo = rational::zero();
+            m_bounds.insert(v, b);
+        }
+        return expr_ref(m.mk_const(v, b.m_int ? a.mk_int() : a.mk_real()), m);
+    }
 
 };
 
-void parse_lp(opt::context& opt, std::istream& is) {
-    lp_stream_buffer _is(is);
-    lp_parse lp(opt, _is);
+void parse_lp(opt::context& opt, std::istream& is, unsigned_vector& h) {
+    opt_stream_buffer _is(is);
+    lp_parse lp(opt, _is, h);
     lp.parse();
 }
 
-#endif
diff --git a/src/opt/opt_parse.h b/src/opt/opt_parse.h
index b058efcac..6cf92bd9c 100644
--- a/src/opt/opt_parse.h
+++ b/src/opt/opt_parse.h
@@ -23,6 +23,8 @@ void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h);
 
 void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h);
 
+void parse_lp(opt::context& opt, std::istream& is, unsigned_vector& h);
+
 #endif /* OPT_PARSE_H_ */
 
 
diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp
index 5e86a7a87..199d12797 100644
--- a/src/sat/sat_watched.cpp
+++ b/src/sat/sat_watched.cpp
@@ -85,7 +85,7 @@ namespace sat {
             }    
         }
         wlist.set_end(it2);
-        VERIFY(found);
+        //VERIFY(found);
     }
 
     void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index fe115611c..58deb7e95 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -38,7 +38,7 @@ Revision History:
 #include "util/env_params.h"
 #include "shell/lp_frontend.h"
 
-typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind;
+typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS } input_kind;
 
 std::string         g_aux_input_file;
 char const *        g_input_file          = 0;
@@ -71,10 +71,12 @@ void display_usage() {
     std::cout << "]. (C) Copyright 2006-2016 Microsoft Corp.\n";
     std::cout << "Usage: z3 [options] [-file:]file\n";
     std::cout << "\nInput format:\n";
-    std::cout << "  -smt        use parser for SMT input format.\n";
     std::cout << "  -smt2       use parser for SMT 2 input format.\n";
     std::cout << "  -dl         use parser for Datalog input format.\n";
     std::cout << "  -dimacs     use parser for DIMACS input format.\n";
+    std::cout << "  -wcnf       use parser for Weighted CNF DIMACS input format.\n";
+    std::cout << "  -opb        use parser for PB optimization input format.\n";
+    std::cout << "  -lp         use parser for a modest subset of CPLEX LP input format.\n";
     std::cout << "  -log        use parser for Z3 log input format.\n";
     std::cout << "  -in         read formula from standard input.\n";
     std::cout << "\nMiscellaneous:\n";
@@ -188,9 +190,12 @@ void parse_cmd_line_args(int argc, char ** argv) {
             else if (strcmp(opt_name, "wcnf") == 0) {
                 g_input_kind = IN_WCNF;
             }
-            else if (strcmp(opt_name, "bpo") == 0) {
+            else if (strcmp(opt_name, "pbo") == 0) {
                 g_input_kind = IN_OPB;
             }
+            else if (strcmp(opt_name, "lp") == 0) {
+                g_input_kind = IN_LP;
+            }
             else if (strcmp(opt_name, "log") == 0) {
                 g_input_kind = IN_Z3_LOG;
             }
@@ -322,6 +327,9 @@ int STD_CALL main(int argc, char ** argv) {
                 else if (strcmp(ext, "opb") == 0) {
                     g_input_kind = IN_OPB;
                 }
+                else if (strcmp(ext, "lp") == 0) {
+                    g_input_kind = IN_LP;
+                }
                 else if (strcmp(ext, "log") == 0) {
                     g_input_kind = IN_Z3_LOG;
                 }
@@ -349,10 +357,13 @@ int STD_CALL main(int argc, char ** argv) {
             return_value = read_dimacs(g_input_file);
             break;
         case IN_WCNF:
-            return_value = parse_opt(g_input_file, true);
+            return_value = parse_opt(g_input_file, wcnf_t);
             break;
         case IN_OPB:
-            return_value = parse_opt(g_input_file, false);
+            return_value = parse_opt(g_input_file, opb_t);
+            break;
+        case IN_LP:
+            return_value = parse_opt(g_input_file, lp_t);
             break;
         case IN_DATALOG:
             read_datalog(g_input_file);
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 8154cbde4..48efd1148 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -14,6 +14,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/timeout.h"
 #include "ast/reg_decl_plugins.h"
 #include "opt/opt_parse.h"
+#include "shell/opt_frontend.h"
 
 extern bool g_display_statistics;
 static bool g_first_interrupt = true;
@@ -73,18 +74,23 @@ static void on_timeout() {
     }
 }
 
-static unsigned parse_opt(std::istream& in, bool is_wcnf) {
+static unsigned parse_opt(std::istream& in, opt_format f) {
     ast_manager m;
     reg_decl_plugins(m);
     opt::context opt(m);
     g_opt = &opt;
     params_ref p = gparams::get_module("opt");
     opt.updt_params(p);
-    if (is_wcnf) {
+    switch (f) {
+    case wcnf_t:
         parse_wcnf(opt, in, g_handles);
-    }
-    else {
+        break;
+    case opb_t:
         parse_opb(opt, in, g_handles);
+        break;
+    case lp_t:
+        parse_lp(opt, in, g_handles);
+        break;
     }
     try {
         lbool r = opt.optimize();
@@ -121,7 +127,7 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
     return 0;
 }
 
-unsigned parse_opt(char const* file_name, bool is_wcnf) {
+unsigned parse_opt(char const* file_name, opt_format f) {
     g_first_interrupt = true;
     g_start_time = static_cast<double>(clock());
     register_on_timeout_proc(on_timeout);
@@ -132,10 +138,10 @@ unsigned parse_opt(char const* file_name, bool is_wcnf) {
             std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
             exit(ERR_OPEN_FILE);
         }
-        return parse_opt(in, is_wcnf);
+        return parse_opt(in, f);
     }
     else {
-        return parse_opt(std::cin, is_wcnf);
+        return parse_opt(std::cin, f);
     }
 }
 
diff --git a/src/shell/opt_frontend.h b/src/shell/opt_frontend.h
index 65ec606a5..1266ed76b 100644
--- a/src/shell/opt_frontend.h
+++ b/src/shell/opt_frontend.h
@@ -13,7 +13,9 @@ Author:
 #ifndef OPT_FRONTEND_H_
 #define OPT_FRONTEND_H_
 
-unsigned parse_opt(char const* file_name, bool is_wcnf);
+enum opt_format { opb_t, wcnf_t, lp_t };
+
+unsigned parse_opt(char const* file_name, opt_format f);
 
 #endif /* OPT_FRONTEND_H_ */
 
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 18acde8a8..4e97b1e57 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -160,11 +160,10 @@ public:
         expr_ref_vector xs(m);
         expr_ref last_v(m);
         if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card");
-        for (unsigned i = 0; i < hi; ++i) {     
-            if (i < lo) {
-                xs.push_back(a.mk_int(1));
-                continue;
-            }
+        if (lo > 0) {
+            xs.push_back(a.mk_int(lo));
+        }
+        for (unsigned i = lo; i < hi; ++i) {     
             std::string name(x->get_decl()->get_name().str());
             expr_ref v(m.mk_fresh_const(name.c_str(), m.mk_bool_sort()), m);
             if (last_v) axioms.push_back(m.mk_implies(v, last_v));
@@ -195,7 +194,7 @@ public:
             if (a.is_int(x) && 
                 is_uninterp_const(x) && 
                 bounds.has_lower(x, lo, s1) && !s1 && lo.is_unsigned() &&
-                bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() <= m_max_ub) {
+                bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() - lo.get_unsigned() <= m_max_ub) {
                 expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned());
                 rep.insert(x, b);
                 m_bounds.insert(x, bound(lo.get_unsigned(), hi.get_unsigned(), b));