diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index 574be63b1..d70675d80 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "model_pp.h"
 #include "front_end_params.h"
 #include "datatype_decl_plugin.h"
+#include "bv_decl_plugin.h"
 #include "pdr_farkas_learner.h"
 #include "ast_smt2_pp.h"
 #include "expr_replacer.h"
@@ -94,9 +95,12 @@ namespace pdr {
         void expand_literals(expr_ref_vector& conjs) {
             arith_util arith(m);
             datatype_util dt(m);
+            bv_util       bv(m);
             expr* e1, *e2, *c, *val;
-            for (unsigned i = 0; i < conjs.size(); ++i) {
+            rational r;
+            unsigned bv_size;
 
+            for (unsigned i = 0; i < conjs.size(); ++i) {
                 expr* e = conjs[i].get();
                 if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
                     conjs[i] = arith.mk_le(e1,e2);
@@ -109,7 +113,8 @@ namespace pdr {
                     }
                     ++i;
                 }
-                else if (m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) {
+                else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
+                         (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
                     func_decl* f = to_app(val)->get_decl();
                     func_decl* r = dt.get_constructor_recognizer(f);
                     conjs[i] = m.mk_app(r,c);
@@ -118,6 +123,24 @@ namespace pdr {
                         conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i)));
                     }
                 }
+                else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
+                         (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
+                    rational two(2);
+                    for (unsigned j = 0; j < bv_size; ++j) {
+                        parameter p(j);
+                        expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
+                        if ((r % two).is_zero()) {
+                            e = m.mk_not(e);
+                        }
+                        r = div(r, two);
+                        if (j == 0) {
+                            conjs[i] = e;
+                        }
+                        else {
+                            conjs.push_back(e);
+                        }
+                    }
+                }
             }
         }
 
@@ -341,7 +364,7 @@ namespace pdr {
         }
         fl.get_lemmas(pr, bs, lemmas);
         safe.elim_proxies(lemmas);
-        fl.simplify_lemmas(lemmas); // redundant
+        fl.simplify_lemmas(lemmas); // redundant?
         if (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
             !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) {
                 IF_VERBOSE(1,