handle ac-op in legacy special relations procedure by adding warning

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 3, 2023 · bd8bed1 · bd8bed1
1 parent 1b1ebaa
commit bd8bed1
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
@@ -130,7 +130,11 @@ namespace smt {
     }
 
     bool theory_special_relations::internalize_term(app * term) {
-        verbose_stream() << mk_pp(term, m) << "\n";
+        m_terms.push_back(term);
+        ctx.push_trail(push_back_vector(m_terms));
+        std::stringstream strm;
+        strm << "term not not handled by special relations procedure. Use sat.smt=true " << mk_pp(term, m);
+        warning_msg(strm.str().c_str());
         return false;
     }
 
@@ -207,9 +211,10 @@ namespace smt {
         if (new_equality) {
             return FC_CONTINUE;
         }
-        else {
+        else if (!m_terms.empty()) 
+            return FC_GIVEUP;
+        else 
             return FC_DONE;
-        }
     }
 
     lbool theory_special_relations::final_check_lo(relation& r) {

diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h
@@ -131,6 +131,7 @@ namespace smt {
         special_relations_util         m_util;
         atoms                          m_atoms;
         unsigned_vector                m_atoms_lim;
+        ptr_vector<app>                m_terms;
         obj_map<func_decl, relation*>  m_relations;
         bool_var2atom                  m_bool_var2atom;
         bool                           m_can_propagate;