From 27e3d28cfc74fa8d3a1788137475652b0e1ca060 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Sep 2024 16:34:35 -0700
Subject: [PATCH] fixing conca

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_eval.cpp |  7 ++++---
 src/ast/sls/sls_bv_fixed.h  | 10 +++++-----
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index 08b9e6baf..b959f0934 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -362,9 +362,9 @@ namespace sls {
         }
         case OP_CONCAT: {
             unsigned bw = 0;
-            for (unsigned i = e->get_num_args(); i-- > 0; ) {
+            for (unsigned i = e->get_num_args(); i-- > 0;) {
                 auto const& a = wval(e->get_arg(i));
-                for (unsigned j = 0; false && j < a.bw; ++j)
+                for (unsigned j = 0; j < a.bw; ++j)
                     val.eval.set(j + bw, a.get_bit(j));
                 bw += a.bw;
             }
@@ -656,7 +656,7 @@ namespace sls {
         }
     }
     
-    bool bv_eval::repair_down(app* e, unsigned i) {      
+    bool bv_eval::repair_down(app* e, unsigned i) {  
         expr* arg = e->get_arg(i);
         if (m.is_value(arg))
             return false;
@@ -1838,6 +1838,7 @@ namespace sls {
         auto& ve = assign_value(e);
         for (unsigned j = e->get_num_args() - 1; j > idx; --j)
             bw += bv.get_bv_size(e->get_arg(j));
+        //verbose_stream() << m_bounded_pp(e, m) << " " << idx << " " << bw << "\n";
         auto& a = wval(e, idx);
         for (unsigned i = 0; i < a.bw; ++i)
             m_tmp.set(i, ve.get(i + bw));
diff --git a/src/ast/sls/sls_bv_fixed.h b/src/ast/sls/sls_bv_fixed.h
index 9b7246e93..d175e9d6a 100644
--- a/src/ast/sls/sls_bv_fixed.h
+++ b/src/ast/sls/sls_bv_fixed.h
@@ -28,11 +28,11 @@ namespace sls {
     class bv_eval;
     
     class bv_fixed {
-        bv_eval&           ev;
-        bv_terms&          terms;
-        ast_manager&        m;
-        bv_util&            bv;
-        sls::context&       ctx;
+        bv_eval&        ev;
+        bv_terms&       terms;
+        ast_manager&    m;
+        bv_util&        bv;
+        sls::context&   ctx;
 
         bool init_range(app* e, bool sign);
         void propagate_range_up(expr* e);