From 3c940b5125cb788d36b7fdda746128d72cdbd3a7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 Jan 2022 17:49:43 +0100
Subject: [PATCH] use nyi to catch uncovered cases

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/solver.cpp | 5 +++--
 src/test/polysat.cpp        | 1 +
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 7cc6f66fd..07191f63c 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -500,8 +500,7 @@ namespace polysat {
         
         search_iterator search_it(m_search);
         while (search_it.next()) {
-            LOG("search state: " << m_search);
-            LOG("Conflict: " << m_conflict);
+            // LOG("search state: " << m_search);
             auto& item = *search_it;
             search_it.set_resolved();
             LOG_H2("Working on " << search_item_pp(m_search, item));
@@ -512,6 +511,7 @@ namespace polysat {
                     m_search.pop_assignment();
                     continue;
                 }
+                LOG("Conflict: " << m_conflict);
                 inc_activity(v);
                 justification& j = m_justification[v];
                 if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
@@ -529,6 +529,7 @@ namespace polysat {
                     continue;
                 if (m_bvars.level(var) <= base_level())  
                     continue;
+                LOG("Conflict: " << m_conflict);
                 if (m_bvars.is_decision(var)) {
                     revert_bool_decision(lit);
                     return;
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 0cd183f09..de2e32dab 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1245,6 +1245,7 @@ public:
             r = alloc(pdd, s.var(s.add_var(sz)));
         else {
             std::cout << "UNKNOWN " << mk_pp(e, m) << "\n";
+            NOT_IMPLEMENTED_YET();
             r = alloc(pdd, s.var(s.add_var(sz)));
         }
         expr2pdd.insert(e, r);