From b56a8fa264808cdc179f660baf08d52fd3093081 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 10 Dec 2023 10:03:43 -0800
Subject: [PATCH] deal with build errors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/euf_solver.cpp                 |  6 +++++-
 src/sat/smt/polysat/polysat_assignment.cpp | 13 +------------
 src/sat/smt/polysat/polysat_assignment.h   |  3 ---
 3 files changed, 6 insertions(+), 16 deletions(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 51c0518e5..2d4b9847e 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -21,6 +21,7 @@ Author:
 #include "sat/smt/sat_smt.h"
 #include "sat/smt/pb_solver.h"
 #include "sat/smt/bv_solver.h"
+#include "sat/smt/polysat_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/array_solver.h"
 #include "sat/smt/arith_solver.h"
@@ -134,8 +135,11 @@ namespace euf {
         special_relations_util sp(m);
         if (pb.get_family_id() == fid)
             ext = alloc(pb::solver, *this, fid);
-        else if (bvu.get_family_id() == fid)
+        else if (bvu.get_family_id() == fid) {
             ext = alloc(bv::solver, *this, fid);
+            dealloc(ext);
+            ext = alloc(polysat::solver, *this, fid);
+        }
         else if (au.get_family_id() == fid)
             ext = alloc(array::solver, *this, fid);
         else if (fpa.get_family_id() == fid)
diff --git a/src/sat/smt/polysat/polysat_assignment.cpp b/src/sat/smt/polysat/polysat_assignment.cpp
index aedf6d409..329733d89 100644
--- a/src/sat/smt/polysat/polysat_assignment.cpp
+++ b/src/sat/smt/polysat/polysat_assignment.cpp
@@ -12,6 +12,7 @@ Author:
 
 --*/
 
+#include <utility>
 #include "sat/smt/polysat/polysat_assignment.h"
 #include "sat/smt/polysat/polysat_core.h"
 
@@ -43,18 +44,6 @@ namespace polysat {
     assignment::assignment(core& s)
         : m_core(s) { }
 
-
-    assignment assignment::clone() const {
-        assignment a(s());
-        a.m_pairs = m_pairs;
-        a.m_subst.reserve(m_subst.size());
-        for (unsigned i = m_subst.size(); i-- > 0; )
-            if (m_subst[i])
-                a.m_subst.set(i, alloc(substitution, *m_subst[i]));
-        a.m_subst_trail = m_subst_trail;
-        return a;
-    }
-
     bool assignment::contains(pvar var) const {
         return subst(s().size(var)).contains(var);
     }
diff --git a/src/sat/smt/polysat/polysat_assignment.h b/src/sat/smt/polysat/polysat_assignment.h
index befaad0b7..559f6dab2 100644
--- a/src/sat/smt/polysat/polysat_assignment.h
+++ b/src/sat/smt/polysat/polysat_assignment.h
@@ -91,9 +91,6 @@ namespace polysat {
         // prevent implicit copy, use clone() if you do need a copy
         assignment(assignment const&) = delete;
         assignment& operator=(assignment const&) = delete;
-        assignment(assignment&&) = default;
-        assignment& operator=(assignment&&) = default;
-        assignment clone() const;
 
         void push(pvar var, rational const& value);
         void pop();