From 8ef4ec7009abaeefa415b1a5b93f020bec3e3ae2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Jun 2014 12:46:23 +0100
Subject: [PATCH] fix bit-vector rotation left bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp |  3 +++
 src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h    | 10 ++++++++--
 src/ast/rewriter/bv_rewriter.cpp                      |  1 +
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 80d319377..63843d31e 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
     
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
+        TRACE("bit_blaster", tout << f->get_name() << " ";
+              for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
+              tout << "\n";);
         if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
             mk_const(f, result);
             return BR_DONE;
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 72c0a447e..b41aa2238 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
 
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
+    TRACE("bit_blaster", tout << n << ": " << sz << " ";
+          for (unsigned i = 0; i < sz; ++i) {
+              tout << mk_pp(a_bits[i], m()) << " ";
+          }
+          tout << "\n";
+          );
     n = n % sz;
     for (unsigned i = sz - n; i < sz; i++) 
         out_bits.push_back(a_bits[i]);
@@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
                 mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
                 out = new_out;
             }
-            TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
+            TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
             out_bits.set(sz - i - 1, out);
         }
     }
@@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
             out = a_bits[i];
             for (unsigned j = 1; j < sz; j++) {
                 expr_ref new_out(m());
-                unsigned src = (Left ? (i - j) : (i + j)) % sz;
+                unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
                 mk_ite(eqs.get(j), a_bits[src], out, new_out);
                 out = new_out;
             }
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 11b09003b..1115663d2 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -21,6 +21,7 @@ Notes:
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
 
+
 mk_extract_proc::mk_extract_proc(bv_util & u):
     m_util(u),
     m_high(0),