From 18280a973798172b7788e2bf09fa0e3df09c0331 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 3 Feb 2020 08:43:45 -0800
Subject: [PATCH] fix #2928 - test case is actually abuse of qe2. It is
 reasonable for qe2 to assume that simplify was applied first

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_bv.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 9eb0dbc06..3442cd369 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -161,7 +161,7 @@ namespace smt {
             e = ctx.mk_enode(n, !m_params.m_bv_reflect, false, m_params.m_bv_cc);
             mk_var(e);
         }
-        SASSERT(e->get_th_var(get_id()) != null_theory_var);
+//        SASSERT(e->get_th_var(get_id()) != null_theory_var);
         return e;
     }