From 7fb2c6a908d5e1a1c4740e0bd3e1b104e33fff19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Feb 2019 15:55:24 +0100 Subject: [PATCH] turn off model validation unless specified by parameter Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 541c4f0f5..779cb7aad 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1788,7 +1788,10 @@ namespace sat { // m_mc.set_solver(nullptr); m_mc(m_model); - + + if (!gparams::get_ref().get_bool("model_validate", false)) { + return; + } if (!check_clauses(m_model)) { IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(10, m_mc.display(verbose_stream()));