fix #3976

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.h

@@ -1899,6 +1899,10 @@ class ast_manager {
         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());
     }

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 {

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)

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();

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;
             }
         }