From 141cd687ffe36f3f94b4de6b7e56eb2f07cbcb03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Nov 2018 15:37:36 -0800 Subject: [PATCH] disable validation in builds Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 6 +++--- src/opt/opt_context.cpp | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 98e6531ea..75a42886c 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -841,7 +841,7 @@ public: } void verify_core(exprs const& core) { - if (!gparams::get_ref().get_bool("model_validate", false)) return; + return; IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); @@ -852,7 +852,7 @@ public: } void verify_assumptions() { - if (!gparams::get_ref().get_bool("model_validate", false)) return; + return; IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); @@ -863,7 +863,7 @@ public: } void verify_assignment() { - if (!gparams::get_ref().get_bool("model_validate", false)) return; + return; IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 29246c6f5..a6f3d8152 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1557,6 +1557,7 @@ namespace opt { } void context::validate_model() { + return; if (!gparams::get_ref().get_bool("model_validate", false)) return; expr_ref_vector fmls(m); get_hard_constraints(fmls);