diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index f4fc71843..b71e4cce9 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -554,6 +554,39 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_ast Z3_API Z3_solver_get_implied_value(Z3_context c, Z3_solver s, Z3_ast e) {
+        Z3_TRY;
+        LOG_Z3_solver_get_implied_value(c, s, e);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        expr_ref v = to_solver_ref(s)->get_implied_value(to_expr(e));
+        mk_c(c)->save_ast_trail(v);
+        RETURN_Z3(of_ast(v));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_solver_get_implied_lower(Z3_context c, Z3_solver s, Z3_ast e) {
+        Z3_TRY;
+        LOG_Z3_solver_get_implied_lower(c, s, e);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        expr_ref v = to_solver_ref(s)->get_implied_lower_bound(to_expr(e));
+        mk_c(c)->save_ast_trail(v);
+        RETURN_Z3(of_ast(v));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_solver_get_implied_upper(Z3_context c, Z3_solver s, Z3_ast e) {
+        Z3_TRY;
+        LOG_Z3_solver_get_implied_upper(c, s, e);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        expr_ref v = to_solver_ref(s)->get_implied_upper_bound(to_expr(e));
+        mk_c(c)->save_ast_trail(v);
+        RETURN_Z3(of_ast(v));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
         for (unsigned i = 0; i < num_assumptions; i++) {
             if (!is_expr(to_ast(assumptions[i]))) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index a5e856142..ac14afe1b 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2379,12 +2379,25 @@ namespace z3 {
         }
         void add(expr const & e, char const * p) {
             add(e, ctx().bool_const(p));
+        }        
+        void add(expr_vector const& v) { 
+            check_context(*this, v); 
+            for (unsigned i = 0; i < v.size(); ++i) 
+                add(v[i]); 
         }
-        // fails for some compilers:
-        // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
         void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
         void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
 
+        expr lower(expr const& e) { 
+            Z3_ast r = Z3_solver_get_implied_lower(ctx(), m_solver, e); check_error(); return expr(ctx(), r); 
+        }
+        expr upper(expr const& e) { 
+            Z3_ast r = Z3_solver_get_implied_upper(ctx(), m_solver, e); check_error(); return expr(ctx(), r); 
+        }
+        expr value(expr const& e) { 
+            Z3_ast r = Z3_solver_get_implied_value(ctx(), m_solver, e); check_error(); return expr(ctx(), r); 
+        }
+
         check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
         check_result check(unsigned n, expr * const assumptions) {
             array<Z3_ast> _assumptions(n);
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index bbf072155..8488f7415 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6857,6 +6857,21 @@ class Solver(Z3PPObject):
         """
         return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
 
+    def value(self, e):
+        """Return value of term in solver, if any is given.
+        """
+        return _to_expr_ref(Z3_solver_get_implied_value(self.ctx.ref(), self.solver, e.as_ast()), self.ctx)
+
+    def lower(self, e):
+        """Return lower bound known to solver based on the last call.
+        """
+        return _to_expr_ref(Z3_solver_get_implied_lower(self.ctx.ref(), self.solver, e.as_ast()), self.ctx)
+    
+    def upper(self, e):
+        """Return upper bound known to solver based on the last call.
+        """
+        return _to_expr_ref(Z3_solver_get_implied_upper(self.ctx.ref(), self.solver, e.as_ast()), self.ctx)
+
     def statistics(self):
         """Return statistics for the last `check()`.
 
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 259c95716..63c7e71e8 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6486,6 +6486,34 @@ extern "C" {
     */
     void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz,  unsigned levels[]);
 
+    /**
+       \brief retrieve implied value for expression, if any is implied by solver at search level.
+       The method works for expressions that are known to the solver state, such as Boolean and
+       arithmetical variables.
+       
+       def_API('Z3_solver_get_implied_value', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_solver_get_implied_value(Z3_context c, Z3_solver s, Z3_ast e);
+
+    /**
+       \brief retrieve implied lower bound value for arithmetic expression.
+       If a lower bound is implied at search level, the arithmetic expression returned
+       is a constant representing the bound.
+       
+       def_API('Z3_solver_get_implied_lower', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_solver_get_implied_lower(Z3_context c, Z3_solver s, Z3_ast e);
+
+    /**
+       \brief retrieve implied upper bound value for arithmetic expression.
+       If an upper bound is implied at search level, the arithmetic expression returned
+       is a constant representing the bound.
+       
+       def_API('Z3_solver_get_implied_upper', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
+    */
+
+    Z3_ast Z3_API Z3_solver_get_implied_upper(Z3_context c, Z3_solver s, Z3_ast e);
+
     /**
        \brief Check whether the assertions in a given solver are consistent or not.
 
diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h
index a153e6af6..409ca3049 100644
--- a/src/muz/spacer/spacer_iuc_solver.h
+++ b/src/muz/spacer/spacer_iuc_solver.h
@@ -123,6 +123,9 @@ public:
     expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
     void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
     expr_ref_vector get_trail() override { return m_solver.get_trail(); }
+    expr_ref get_implied_value(expr* e) override { return m_solver.get_implied_value(e); }
+    expr_ref get_implied_lower_bound(expr* e) override { return m_solver.get_implied_lower_bound(e); }
+    expr_ref get_implied_upper_bound(expr* e) override { return m_solver.get_implied_upper_bound(e); }
 
     void push() override;
     void pop(unsigned n) override;
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 6442448cc..b6b35dd3c 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -111,6 +111,9 @@ namespace opt {
         void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override; 
         expr_ref_vector get_trail() override { return m_context.get_trail(); }
         expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
+        expr_ref get_implied_value(expr* e) override { return m_context.get_implied_value(e); }
+        expr_ref get_implied_lower_bound(expr* e) override { return m_context.get_implied_lower_bound(e); }
+        expr_ref get_implied_upper_bound(expr* e) override { return m_context.get_implied_upper_bound(e); }
 
         void set_logic(symbol const& logic);
 
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 20484ae28..4bb9563e9 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -363,6 +363,19 @@ public:
         return nullptr;
     }
 
+    // TODO
+    expr_ref get_implied_value(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_lower_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_upper_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
     expr_ref_vector last_cube(bool is_sat) {
         expr_ref_vector result(m);
         result.push_back(is_sat ? m.mk_true() : m.mk_false());
diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp
index abf7161da..a5a59f60f 100644
--- a/src/smt/smt_arith_value.cpp
+++ b/src/smt/smt_arith_value.cpp
@@ -125,9 +125,37 @@ namespace smt {
         return false;
     }
 
+    expr_ref arith_value::get_lo(expr* e) const {
+        rational lo;
+        bool s = false;
+        if (a.is_int_real(e) && get_lo(e, lo, s) && !s) {
+            return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m);
+        }
+        return expr_ref(e, m);
+    }
+
+    expr_ref arith_value::get_up(expr* e) const {
+        rational up;
+        bool s = false;
+        if (a.is_int_real(e) && get_up(e, up, s) && !s) {
+            return expr_ref(a.mk_numeral(up, m.get_sort(e)), m);
+        }
+        return expr_ref(e, m);
+    }
+
+    expr_ref arith_value::get_fixed(expr* e) const {
+        rational lo, up;
+        bool s = false;
+        if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) {
+            return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m);
+        }
+        return expr_ref(e, m);
+    }    
+
     final_check_status arith_value::final_check() {
         family_id afid = a.get_family_id();
         theory * th = m_ctx->get_theory(afid);
         return th->final_check_eh();
     }
+
 };
diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h
index ab81a77d9..a204cad8c 100644
--- a/src/smt/smt_arith_value.h
+++ b/src/smt/smt_arith_value.h
@@ -42,6 +42,9 @@ namespace smt {
         bool get_lo(expr* e, rational& lo, bool& strict) const;
         bool get_up(expr* e, rational& up, bool& strict) const;
         bool get_value(expr* e, rational& value) const;
+        expr_ref get_lo(expr* e) const;
+        expr_ref get_up(expr* e) const;
+        expr_ref get_fixed(expr* e) const;
         final_check_status final_check();
     };
 };
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 5a418e38d..eeb8cafc0 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -39,6 +39,7 @@ Revision History:
 #include "smt/smt_model_checker.h"
 #include "smt/smt_model_finder.h"
 #include "smt/smt_parallel.h"
+#include "smt/smt_arith_value.h"
 
 namespace smt {
 
@@ -4555,6 +4556,48 @@ namespace smt {
         TRACE("model", tout << *m_model << "\n";);
     }
 
+    expr_ref context::get_implied_value(expr* e) {
+        pop_to_search_lvl();
+        if (m.is_bool(e)) {
+            if (b_internalized(e)) {
+                bool_var v = get_bool_var(e);
+                switch (get_assignment(get_bool_var(e))) {
+                case l_true: e = m.mk_true(); break;
+                case l_false: e = m.mk_false(); break;
+                default: break;
+                }
+            }
+            return expr_ref(e, m);
+        }
+
+        if (e_internalized(e)) {
+            enode* n = get_enode(e);
+            for (enode* r : *n) {
+                if (m.is_value(r->get_owner())) {
+                    return expr_ref(r->get_owner(), m);
+                }
+            }
+        }
+
+        arith_value av(m);
+        av.init(this);
+        return av.get_fixed(e);
+    }
+
+    expr_ref context::get_implied_lower_bound(expr* e) {
+        pop_to_search_lvl();
+        arith_value av(m);
+        av.init(this);
+        return av.get_lo(e);
+    }
+
+    expr_ref context::get_implied_upper_bound(expr* e) {
+        pop_to_search_lvl();
+        arith_value av(m);
+        av.init(this);
+        return av.get_up(e);
+    }
+
 };
 
 
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index dac44365f..cf06b4858 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -580,6 +580,13 @@ namespace smt {
             return get_bdata(v).get_theory();
         }
 
+        expr_ref get_implied_value(expr* e);
+
+        expr_ref get_implied_lower_bound(expr* e);
+
+        expr_ref get_implied_upper_bound(expr* e);
+
+
         friend class set_var_theory_trail;
         void set_var_theory(bool_var v, theory_id tid);
 
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index bd25e2592..de785cfae 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -131,6 +131,18 @@ namespace smt {
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
             return m_kernel.find_mutexes(vars, mutexes);
         }
+
+        expr_ref get_implied_value(expr* e) {
+            return m_kernel.get_implied_value(e);
+        }
+
+        expr_ref get_implied_lower_bound(expr* e) {
+            return m_kernel.get_implied_lower_bound(e);
+        }
+
+        expr_ref get_implied_upper_bound(expr* e) {
+            return m_kernel.get_implied_upper_bound(e);
+        }
         
         void get_model(model_ref & m) {
             m_kernel.get_model(m);
@@ -412,5 +424,18 @@ namespace smt {
         return m_imp->get_trail();
     }
 
+    expr_ref kernel::get_implied_value(expr* e) {
+        return m_imp->get_implied_value(e);
+    }
+    
+    expr_ref kernel::get_implied_lower_bound(expr* e) {
+        return m_imp->get_implied_lower_bound(e);
+    }
+    
+    expr_ref kernel::get_implied_upper_bound(expr* e) {
+        return m_imp->get_implied_upper_bound(e);
+    }
+
+
 
 };
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 73797633e..f210d69ec 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -218,6 +218,17 @@ namespace smt {
         */
         expr_ref next_cube();
 
+        /**
+           \brief retrieve upper/lower bound for arithmetic term, if it is implied.
+           retrieve implied values if terms are fixed to a value.
+        */
+
+        expr_ref get_implied_value(expr* e);
+
+        expr_ref get_implied_lower_bound(expr* e);
+
+        expr_ref get_implied_upper_bound(expr* e);
+
         /**
            \brief retrieve depth of variables from decision stack.
         */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 84d9894fc..2ebd0c967 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -361,6 +361,18 @@ namespace {
             }
         }
 
+        expr_ref get_implied_value(expr* e) override {
+            return m_context.get_implied_value(e);
+        }
+
+        expr_ref get_implied_lower_bound(expr* e) override {
+            return m_context.get_implied_lower_bound(e);
+        }
+
+        expr_ref get_implied_upper_bound(expr* e) override {
+            return m_context.get_implied_upper_bound(e);
+        }
+
         bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) {
             for (func_decl * fd : pattern_fds) {
                 if (assrtn_fds.contains(fd))
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ea2f053c4..cd8abd346 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1724,6 +1724,7 @@ public:
             is_sat = make_feasible();
         }
         final_check_status st = FC_DONE;
+
         switch (is_sat) {
         case l_true:
             TRACE("arith", /*display(tout);*/
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 267a22de0..19b1c9351 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -184,6 +184,28 @@ public:
         return m_solver1->get_scope_level();
     }
 
+    expr_ref get_implied_value(expr* e) override {
+        if (m_use_solver1_results)
+            return m_solver1->get_implied_value(e);
+        else
+            return m_solver2->get_implied_value(e);
+    }
+    
+    expr_ref get_implied_lower_bound(expr* e) override {
+        if (m_use_solver1_results)
+            return m_solver1->get_implied_lower_bound(e);
+        else
+            return m_solver2->get_implied_lower_bound(e);
+    }
+    
+    expr_ref get_implied_upper_bound(expr* e) override {
+        if (m_use_solver1_results)
+            return m_solver1->get_implied_upper_bound(e);
+        else
+            return m_solver2->get_implied_upper_bound(e);
+    }
+
+
     lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
         switch_inc_mode();
         m_use_solver1_results = false;
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 42a3f3cbd..e3d980021 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -226,6 +226,19 @@ public:
 
     virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) = 0;
 
+    /**
+       \brief retrieve fixed value assignment in current solver state, if it is implied.
+    */
+    virtual expr_ref get_implied_value(expr* e) = 0;
+
+    /**
+       \brief retrieve upper/lower bound for arithmetic term, if it is implied.
+    */
+    virtual expr_ref get_implied_lower_bound(expr* e) = 0;
+
+    virtual expr_ref get_implied_upper_bound(expr* e) = 0;
+
+
     /**
        \brief Display the content of this solver.
     */
diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index 16764ba56..4cd6a5258 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -127,6 +127,18 @@ public:
         return m_base->get_trail();
     }
 
+    expr_ref get_implied_value(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_lower_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_upper_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
     lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
         SASSERT(!m_pushed || get_scope_level() > 0);
         m_proof.reset();
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index f1fcc8567..8456b1254 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -97,6 +97,17 @@ public:
         throw default_exception("cannot retrieve trail from solvers created using tactcis");
     }
 
+    expr_ref get_implied_value(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_lower_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_upper_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
 
 };
 
diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
index ca40607d4..f872d1f5c 100644
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@@ -361,6 +361,18 @@ private:
         }
     }
 
+    expr_ref get_implied_value(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_lower_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_upper_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
 };
 
 solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp
index d8119ddfd..3410f4062 100644
--- a/src/tactic/fd_solver/enum2bv_solver.cpp
+++ b/src/tactic/fd_solver/enum2bv_solver.cpp
@@ -194,6 +194,18 @@ public:
         return m_solver->get_assertion(idx);
     }
 
+    expr_ref get_implied_value(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_lower_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_upper_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
 };
 
 solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) {
diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp
index 9e17dd711..20e0bc545 100644
--- a/src/tactic/fd_solver/pb2bv_solver.cpp
+++ b/src/tactic/fd_solver/pb2bv_solver.cpp
@@ -147,6 +147,18 @@ public:
         return m_solver->get_assertion(idx);
     }
 
+    expr_ref get_implied_value(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_lower_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
+    expr_ref get_implied_upper_bound(expr* e) override {
+        return expr_ref(e, m);
+    }
+
 
 private:
     void flush_assertions() const {
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 8ba9dc44d..84c10c28b 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -2103,6 +2103,19 @@ namespace smtfd {
         expr * get_assertion(unsigned idx) const override {
             return m_assertions.get(idx);
         }
+
+        expr_ref get_implied_value(expr* e) override {
+            return expr_ref(e, m);
+        }
+        
+        expr_ref get_implied_lower_bound(expr* e) override {
+            return expr_ref(e, m);
+        }
+        
+        expr_ref get_implied_upper_bound(expr* e) override {
+            return expr_ref(e, m);
+        }
+
     };
 
 }