From f8c593edf9a837043ea6d4a3cc0effaf6bd45931 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 23 Apr 2024 14:38:33 +0200
Subject: [PATCH] remove unused ckind_t::smul_fl_t

---
 src/sat/smt/polysat/constraints.h | 3 +--
 src/sat/smt/polysat_solver.cpp    | 3 ---
 2 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h
index f6ad6b053..23e801ce1 100644
--- a/src/sat/smt/polysat/constraints.h
+++ b/src/sat/smt/polysat/constraints.h
@@ -29,7 +29,7 @@ namespace polysat {
     using pdd = dd::pdd;
     using pvar = unsigned;
 
-    enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t };
+    enum ckind_t { ule_t, umul_ovfl_t, op_t };
 
     class constraint {
         unsigned_vector     m_vars;
@@ -86,7 +86,6 @@ namespace polysat {
         ckind_t op() const { return m_op; }
         bool is_ule() const { return m_op == ule_t; }
         bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
-        bool is_smul_fl() const { return m_op == smul_fl_t; }
         bool is_op() const { return m_op == op_t; }
         ule_constraint const& to_ule() const { SASSERT(is_ule()); return *reinterpret_cast<ule_constraint*>(m_constraint); }
         umul_ovfl_constraint const& to_umul_ovfl() const { SASSERT(is_umul_ovfl()); return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 5600e6590..6d75a627c 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -477,9 +477,6 @@ namespace polysat {
         case ckind_t::op_t:
             UNREACHABLE();
             break;
-        case ckind_t::smul_fl_t:
-            NOT_IMPLEMENTED_YET();
-            break;
         }
         return result;
     }