diff --git a/src/sat/smt/polysat/CMakeLists.txt b/src/sat/smt/polysat/CMakeLists.txt
index 6c8bed74d..1f943f48d 100644
--- a/src/sat/smt/polysat/CMakeLists.txt
+++ b/src/sat/smt/polysat/CMakeLists.txt
@@ -1,13 +1,13 @@
 z3_add_component(polysat
   SOURCES
+    assignment.cpp
+    constraints.cpp
+    core.cpp
     fixed_bits.cpp
-    polysat_assignment.cpp
-    polysat_constraints.cpp
-    polysat_core.cpp
-    polysat_fi.cpp
-    polysat_ule.cpp
-    polysat_umul_ovfl.cpp
-    polysat_viable.cpp
+    forbidden_intervals.cpp
+    ule_constraint.cpp
+    umul_ovfl_constraint.cpp
+    viable.cpp
   COMPONENT_DEPENDENCIES
     util
     dd
diff --git a/src/sat/smt/polysat/polysat_assignment.cpp b/src/sat/smt/polysat/assignment.cpp
similarity index 97%
rename from src/sat/smt/polysat/polysat_assignment.cpp
rename to src/sat/smt/polysat/assignment.cpp
index 329733d89..c1620891a 100644
--- a/src/sat/smt/polysat/polysat_assignment.cpp
+++ b/src/sat/smt/polysat/assignment.cpp
@@ -13,8 +13,8 @@ Author:
 --*/
 
 #include <utility>
-#include "sat/smt/polysat/polysat_assignment.h"
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/assignment.h"
+#include "sat/smt/polysat/core.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_assignment.h b/src/sat/smt/polysat/assignment.h
similarity index 98%
rename from src/sat/smt/polysat/polysat_assignment.h
rename to src/sat/smt/polysat/assignment.h
index 559f6dab2..823d991b9 100644
--- a/src/sat/smt/polysat/polysat_assignment.h
+++ b/src/sat/smt/polysat/assignment.h
@@ -13,7 +13,7 @@ Author:
 --*/
 #pragma once
 #include "util/scoped_ptr_vector.h"
-#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/types.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_constraints.cpp b/src/sat/smt/polysat/constraints.cpp
similarity index 91%
rename from src/sat/smt/polysat/polysat_constraints.cpp
rename to src/sat/smt/polysat/constraints.cpp
index faeea62a4..0de987693 100644
--- a/src/sat/smt/polysat/polysat_constraints.cpp
+++ b/src/sat/smt/polysat/constraints.cpp
@@ -13,10 +13,10 @@ Author:
 --*/
 
 #include "util/log.h"
-#include "sat/smt/polysat/polysat_core.h"
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_ule.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/core.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/ule_constraint.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_constraints.h b/src/sat/smt/polysat/constraints.h
similarity index 99%
rename from src/sat/smt/polysat/polysat_constraints.h
rename to src/sat/smt/polysat/constraints.h
index fdef902e2..81ba6f6a0 100644
--- a/src/sat/smt/polysat/polysat_constraints.h
+++ b/src/sat/smt/polysat/constraints.h
@@ -15,7 +15,7 @@ Author:
 
 #pragma once 
 #include "util/trail.h"
-#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/types.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_core.cpp b/src/sat/smt/polysat/core.cpp
similarity index 95%
rename from src/sat/smt/polysat/polysat_core.cpp
rename to src/sat/smt/polysat/core.cpp
index 13964720d..8e779923d 100644
--- a/src/sat/smt/polysat/polysat_core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -28,7 +28,7 @@ polysat::core
 
 --*/
 
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/core.h"
 
 namespace polysat {
 
@@ -335,4 +335,15 @@ namespace polysat {
         return s.trail();
     }
 
+    std::ostream& core::display(std::ostream& out) const {
+        if (m_constraint_index.empty() && m_vars.empty())
+            return out;
+        out << "polysat:\n";
+        for (auto const& [sc, d, value] : m_constraint_index) 
+            out << sc << " " << d << " := " << value << "\n";        
+        for (unsigned i = 0; i < m_vars.size(); ++i) 
+            out << "p" << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";
+        return out;
+    }
+
 }
diff --git a/src/sat/smt/polysat/polysat_core.h b/src/sat/smt/polysat/core.h
similarity index 95%
rename from src/sat/smt/polysat/polysat_core.h
rename to src/sat/smt/polysat/core.h
index 4e9c02118..32ad84fa3 100644
--- a/src/sat/smt/polysat/polysat_core.h
+++ b/src/sat/smt/polysat/core.h
@@ -21,10 +21,10 @@ Author:
 #include "util/dependency.h"
 #include "math/dd/dd_pdd.h"
 #include "sat/sat_extension.h"
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_viable.h"
-#include "sat/smt/polysat/polysat_assignment.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/viable.h"
+#include "sat/smt/polysat/assignment.h"
 
 namespace polysat {
 
@@ -136,7 +136,7 @@ namespace polysat {
         constraints& cs() { return m_constraints; }
         trail_stack& trail();
 
-        std::ostream& display(std::ostream& out) const { NOT_IMPLEMENTED_YET();  throw default_exception("nyi"); }
+        std::ostream& display(std::ostream& out) const;
     };
 
 }
diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 9b67c883d..85b35de66 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -12,7 +12,7 @@ Author:
 --*/
 
 #include "sat/smt/polysat/fixed_bits.h"
-#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/ule_constraint.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/fixed_bits.h b/src/sat/smt/polysat/fixed_bits.h
index 78b4a643f..f07b2c7d2 100644
--- a/src/sat/smt/polysat/fixed_bits.h
+++ b/src/sat/smt/polysat/fixed_bits.h
@@ -11,8 +11,8 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/constraints.h"
 #include "util/vector.h"
 
 namespace polysat {
diff --git a/src/sat/smt/polysat/polysat_fi.cpp b/src/sat/smt/polysat/forbidden_intervals.cpp
similarity index 98%
rename from src/sat/smt/polysat/polysat_fi.cpp
rename to src/sat/smt/polysat/forbidden_intervals.cpp
index e54fb5cea..1c0494429 100644
--- a/src/sat/smt/polysat/polysat_fi.cpp
+++ b/src/sat/smt/polysat/forbidden_intervals.cpp
@@ -13,11 +13,11 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
 
 --*/
-#include "sat/smt/polysat/polysat_fi.h"
-#include "sat/smt/polysat/polysat_interval.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
-#include "sat/smt/polysat/polysat_ule.h"
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/forbidden_intervals.h"
+#include "sat/smt/polysat/interval.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
+#include "sat/smt/polysat/ule_constraint.h"
+#include "sat/smt/polysat/core.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_fi.h b/src/sat/smt/polysat/forbidden_intervals.h
similarity index 96%
rename from src/sat/smt/polysat/polysat_fi.h
rename to src/sat/smt/polysat/forbidden_intervals.h
index e1f876c3c..b790da1c8 100644
--- a/src/sat/smt/polysat/polysat_fi.h
+++ b/src/sat/smt/polysat/forbidden_intervals.h
@@ -14,9 +14,9 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_interval.h"
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/interval.h"
+#include "sat/smt/polysat/constraints.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_interval.h b/src/sat/smt/polysat/interval.h
similarity index 99%
rename from src/sat/smt/polysat/polysat_interval.h
rename to src/sat/smt/polysat/interval.h
index 0299f83b3..27e62eef9 100644
--- a/src/sat/smt/polysat/polysat_interval.h
+++ b/src/sat/smt/polysat/interval.h
@@ -12,7 +12,7 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/types.h"
 #include <optional>
 
 namespace polysat {
diff --git a/src/sat/smt/polysat/polysat_types.h b/src/sat/smt/polysat/types.h
similarity index 100%
rename from src/sat/smt/polysat/polysat_types.h
rename to src/sat/smt/polysat/types.h
diff --git a/src/sat/smt/polysat/polysat_ule.cpp b/src/sat/smt/polysat/ule_constraint.cpp
similarity index 99%
rename from src/sat/smt/polysat/polysat_ule.cpp
rename to src/sat/smt/polysat/ule_constraint.cpp
index 7482ec36a..3d6240bad 100644
--- a/src/sat/smt/polysat/polysat_ule.cpp
+++ b/src/sat/smt/polysat/ule_constraint.cpp
@@ -70,8 +70,8 @@ Useful lemmas:
 
 --*/
 
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/ule_constraint.h"
 
 #define LOG(_msg_) verbose_stream() << _msg_ << "\n"
 
diff --git a/src/sat/smt/polysat/polysat_ule.h b/src/sat/smt/polysat/ule_constraint.h
similarity index 95%
rename from src/sat/smt/polysat/polysat_ule.h
rename to src/sat/smt/polysat/ule_constraint.h
index 2944bf614..0d481c5ea 100644
--- a/src/sat/smt/polysat/polysat_ule.h
+++ b/src/sat/smt/polysat/ule_constraint.h
@@ -12,8 +12,8 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_assignment.h"
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/assignment.h"
+#include "sat/smt/polysat/constraints.h"
 
 
 namespace polysat {
diff --git a/src/sat/smt/polysat/polysat_umul_ovfl.cpp b/src/sat/smt/polysat/umul_ovfl_constraint.cpp
similarity index 92%
rename from src/sat/smt/polysat/polysat_umul_ovfl.cpp
rename to src/sat/smt/polysat/umul_ovfl_constraint.cpp
index dfe400603..e7dc5801c 100644
--- a/src/sat/smt/polysat/polysat_umul_ovfl.cpp
+++ b/src/sat/smt/polysat/umul_ovfl_constraint.cpp
@@ -10,9 +10,9 @@ Author:
     Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
 
 --*/
-#include "sat/smt/polysat/polysat_constraints.h"
-#include "sat/smt/polysat/polysat_assignment.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/constraints.h"
+#include "sat/smt/polysat/assignment.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
 
 
 namespace polysat {
diff --git a/src/sat/smt/polysat/polysat_umul_ovfl.h b/src/sat/smt/polysat/umul_ovfl_constraint.h
similarity index 96%
rename from src/sat/smt/polysat/polysat_umul_ovfl.h
rename to src/sat/smt/polysat/umul_ovfl_constraint.h
index 65a12c031..4ac03dfb3 100644
--- a/src/sat/smt/polysat/polysat_umul_ovfl.h
+++ b/src/sat/smt/polysat/umul_ovfl_constraint.h
@@ -11,7 +11,7 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/constraints.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_viable.cpp b/src/sat/smt/polysat/viable.cpp
similarity index 99%
rename from src/sat/smt/polysat/polysat_viable.cpp
rename to src/sat/smt/polysat/viable.cpp
index a24683ade..20a31b730 100644
--- a/src/sat/smt/polysat/polysat_viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -18,9 +18,9 @@ Notes:
 
 #include "util/debug.h"
 #include "util/log.h"
-#include "sat/smt/polysat/polysat_viable.h"
-#include "sat/smt/polysat/polysat_core.h"
-#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/viable.h"
+#include "sat/smt/polysat/core.h"
+#include "sat/smt/polysat/ule_constraint.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_viable.h b/src/sat/smt/polysat/viable.h
similarity index 99%
rename from src/sat/smt/polysat/polysat_viable.h
rename to src/sat/smt/polysat/viable.h
index 88070a553..5f5af7616 100644
--- a/src/sat/smt/polysat/polysat_viable.h
+++ b/src/sat/smt/polysat/viable.h
@@ -21,8 +21,8 @@ Author:
 #include "util/map.h"
 #include "util/small_object_allocator.h"
 
-#include "sat/smt/polysat/polysat_types.h"
-#include "sat/smt/polysat/polysat_fi.h"
+#include "sat/smt/polysat/types.h"
+#include "sat/smt/polysat/forbidden_intervals.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index e4e022c6e..82a61486a 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -27,8 +27,8 @@ The result of polysat::core::check is one of:
 #include "ast/euf/euf_bv_plugin.h"
 #include "sat/smt/polysat_solver.h"
 #include "sat/smt/euf_solver.h"
-#include "sat/smt/polysat/polysat_ule.h"
-#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/ule_constraint.h"
+#include "sat/smt/polysat/umul_ovfl_constraint.h"
 
 
 
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 1d1356b0e..5a9c26cb8 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -18,7 +18,7 @@ Author:
 
 #include "sat/smt/sat_th.h"
 #include "math/dd/dd_pdd.h"
-#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/core.h"
 #include "sat/smt/intblast_solver.h"
 
 namespace euf {