From 0b424942abb90a51220e70f6e7cab30ff2e18fe5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Dec 2017 14:42:21 -0800 Subject: [PATCH] bug fixes Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 6 +----- src/util/resource_limit.h | 2 +- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index bcd264743..257cf3b53 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -983,11 +983,7 @@ void sat2goal::mc::operator()(expr_ref& fml) { } void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { - if (m_var2expr.get(v, nullptr)) { - std::cout << mk_pp(atom, m) << "\n"; - std::cout << mk_pp(m_var2expr.get(v, nullptr), m) << "\n"; - } - VERIFY(!m_var2expr.get(v, nullptr)); + SASSERT(!m_var2expr.get(v, nullptr)); m_var2expr.reserve(v + 1); m_var2expr.set(v, atom); if (aux) { diff --git a/src/util/resource_limit.h b/src/util/resource_limit.h index 969953aaf..3f5c4d520 100644 --- a/src/util/resource_limit.h +++ b/src/util/resource_limit.h @@ -1,7 +1,7 @@ /*++ Copyright (c) 2006 Microsoft Corporation -Modulre Name: +Module Name: resource_limit.h