Add groovy R.U.Stan option to retrieve models even when they don't exist #4924

Usage:
z3 4924.smt2 smt.candidate_models=true

src/smt/params/smt_params_helper.pyg

@@ -20,6 +20,7 @@ def_module_params(module_name='smt',
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
+	                  ('candidate_models', BOOL, False, 'create candidate models even when quantifier or theory reasoning is incomplete'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
 	                  ('cube_depth', UINT, 1, 'cube depth.'),

src/smt/smt_solver.cpp

@@ -16,16 +16,17 @@ Author:
 Notes:
 
 --*/
-#include "solver/solver_na2as.h"
-#include "smt/smt_kernel.h"
+
+#include "util/dec_ref_util.h"
 #include "ast/reg_decl_plugins.h"
-#include "smt/params/smt_params.h"
-#include "smt/params/smt_params_helper.hpp"
-#include "solver/mus.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/func_decl_dependencies.h"
-#include "util/dec_ref_util.h"
+#include "smt/smt_kernel.h"
+#include "smt/params/smt_params.h"
+#include "smt/params/smt_params_helper.hpp"
+#include "solver/solver_na2as.h"
+#include "solver/mus.h"
 
 namespace {
 

src/smt/tactic/smt_tactic.cpp

@@ -72,7 +72,8 @@ public:
     }
 
     void updt_params_core(params_ref const & p) {
-        m_candidate_models     = p.get_bool("candidate_models", false);
+        smt_params_helper _p(p);
+        m_candidate_models     = _p.candidate_models();
         m_fail_if_inconclusive = p.get_bool("fail_if_inconclusive", true);
     }
 
@@ -89,7 +90,6 @@ public:
     }
 
     void collect_param_descrs(param_descrs & r) override {
-        r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete.");
         r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal.");
         smt_params_helper::collect_param_descrs(r);
     }