From 4a9c4ca2ce7d85d8fe0023ba48d8b38107334731 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Jul 2023 14:12:29 -0700 Subject: [PATCH] initialize poly solver in incremental mode Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e55208575..7902a3440 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -36,6 +36,7 @@ Revision History: #include "smt/smt_quick_checker.h" #include "smt/uses_theory.h" #include "smt/theory_special_relations.h" +#include "smt/theory_polymorphism.h" #include "smt/smt_for_each_relevant_expr.h" #include "smt/smt_model_generator.h" #include "smt/smt_model_checker.h" @@ -3703,6 +3704,8 @@ namespace smt { m_phase_default = false; m_case_split_queue ->init_search_eh(); m_next_progress_sample = 0; + if (m.has_type_vars() && !m_theories.get_plugin(poly_family_id)) + register_plugin(alloc(theory_polymorphism, *this)); TRACE("literal_occ", display_literal_num_occs(tout);); }