From cce27ff65ffc7c071e2c29cad6f4dd2bfb07239b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Apr 2020 07:53:46 -0700
Subject: [PATCH] fix #3976

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h                    | 4 ++++
 src/ast/datatype_decl_plugin.cpp | 4 ++--
 src/cmd_context/pdecl.cpp        | 1 +
 src/smt/params/smt_params.cpp    | 2 ++
 src/smt/qi_queue.cpp             | 6 +++---
 5 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 52987b785..ece6d0005 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1899,6 +1899,10 @@ public:
         return mk_app(decl, args.size(), args.c_ptr());
     }
 
+    app * mk_app(func_decl * decl, ptr_buffer<expr> const& args) {
+        return mk_app(decl, args.size(), args.c_ptr());
+    }
+
     app * mk_app(func_decl * decl, ptr_vector<app> const& args) {
         return mk_app(decl, args.size(), (expr*const*)args.c_ptr());
     }
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 76c25e2c5..1ab438e72 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -623,7 +623,7 @@ namespace datatype {
             for (unsigned i = 0; i < c->get_arity(); i++) {
                 args.push_back(m_manager->get_some_value(c->get_domain(i)));
             }
-            return m_manager->mk_app(c, args.size(), args.c_ptr());
+            return m_manager->mk_app(c, args);
         }
 
         bool plugin::is_fully_interp(sort * s) const {
@@ -1045,7 +1045,7 @@ namespace datatype {
     }
 
     app* util::mk_is(func_decl * c, expr *f) {
-        return m.mk_app(get_constructor_is(c), 1, &f);
+        return m.mk_app(get_constructor_is(c), f);
     }
 
     func_decl * util::get_recognizer_constructor(func_decl * recognizer) const {
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index ec9a6a367..c9fb42f9a 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -682,6 +682,7 @@ bool pdatatypes_decl::fix_missing_refs(symbol & missing) {
 
 sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s) {
     TRACE("datatype", tout << name << " "; for (unsigned i = 0; i < n; ++i) tout << s[i]->get_name() << " "; tout << "\n";);
+
     pdecl_manager& m = *this;
     sort * r = p->find(s);
     if (r)
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 51225e690..650200bab 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -28,7 +28,9 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_ematching   = p.ematching();
     m_clause_proof = p.clause_proof();
     m_phase_selection = static_cast<phase_selection>(p.phase_selection());
+    if (m_phase_selection > PS_THEORY) throw default_exception("illegal phase selection numeral");
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
+    if (m_restart_strategy > RS_ARITHMETIC) throw default_exception("illegal restart strategy numeral");
     m_restart_factor = p.restart_factor();
     m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
     m_theory_case_split = p.theory_case_split();
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 9611d8485..98301d6d4 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -150,6 +150,9 @@ namespace smt {
     void qi_queue::instantiate() {
         unsigned since_last_check = 0;
         for (entry & curr : m_new_entries) {
+            if (m_context.get_cancel_flag()) {
+                break;
+            }
             fingerprint * f    = curr.m_qb;
             quantifier * qa    = static_cast<quantifier*>(f->get_data());
 
@@ -171,9 +174,6 @@ namespace smt {
                 if (m_context.resource_limits_exceeded()) {
                     break;
                 }
-                if (m_context.get_cancel_flag()) {
-                    break;
-                }
                 since_last_check = 0;
             }
         }