From 124e963b10d25d711c7c951be862ad81fa926de7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Jul 2018 16:26:41 -0700
Subject: [PATCH] revert bit-resize issues

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

diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 70438d1b1..e693c4531 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -37,7 +37,6 @@ namespace smt {
         m_wpos.push_back(0);
         m_zero_one_bits.push_back(zero_one_bits());
         get_context().attach_th_var(n, this, r);
-        mk_bits(r);
         return r;
     }
 
@@ -162,6 +161,7 @@ namespace smt {
         theory_var v = n->get_th_var(get_id());
         if (v == null_theory_var) {
             v = mk_var(n);
+            mk_bits(v);
         }
         return v;
     }
@@ -1092,7 +1092,7 @@ namespace smt {
 
     void theory_bv::apply_sort_cnstr(enode * n, sort * s) {
         if (!is_attached_to_var(n) && !approximate_term(n->get_owner())) {
-            mk_var(n);
+            mk_bits(mk_var(n));
         }
     }