From 912b284602d8efda658de4706405e7f3fedc9b57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Aug 2022 19:07:55 -0700 Subject: [PATCH] disable validate_hint too permissive --- src/shell/drat_frontend.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index f4073b145..0cdac2953 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -459,7 +459,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) { std::cout.flush(); switch (r.m_tag) { case dimacs::drat_record::tag_t::is_clause: { - bool validated = checker.validate_hint(exprs, r.m_lits, r.m_hint); + bool validated = false && checker.validate_hint(exprs, r.m_lits, r.m_hint); checker.add(r.m_lits, r.m_status, validated); if (drat_checker.inconsistent()) { std::cout << "inconsistent\n";