From ab668cbe6c642e459436ec1cddc1f4d4913f97bd 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                 |  1 +
 src/sat/smt/polysat/polysat_assignment.cpp | 13 +------------
 src/sat/smt/polysat/polysat_assignment.h   |  3 ---
 3 files changed, 2 insertions(+), 15 deletions(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index ff11b0749..729ad81e8 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -22,6 +22,7 @@ Author:
 #include "sat/smt/pb_solver.h"
 #include "sat/smt/bv_solver.h"
 #include "sat/smt/intblast_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"
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();