From 2a8c7a7cd7869f6ec685e68dd0d194180965101b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Mar 2023 16:02:09 -0700
Subject: [PATCH] build issue for linux/clang

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

diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index e27cc0f58..6eae5ae7c 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -68,18 +68,16 @@ namespace bv {
             kind_t     m_kind;
             union {
                 // for eq2bit, ne2bit, bit2eq, bit2ne, bv2int:
+                sat::literal m_consequent;
+                sat::literal m_antecedent;
                 struct {
                     unsigned   m_idx;
                     theory_var m_v1;
                     theory_var m_v2;
-                    sat::literal m_consequent;
-                    sat::literal m_antecedent;
                     euf::enode* a, *b, *c;
                 };
                 // for bvext:
                 struct {
-                    // sat::literal     m_consequent; // literal consequent for propagations
-                    // euf::enode_pair  m_eq;         // equality consequent for propagations
                     unsigned         m_num_literals;
                     unsigned         m_num_eqs;        
                     sat::literal*    m_literals;