From 7ada6c25d95403d46731c104de9dc5b7c6cb94c6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 31 Jan 2018 11:10:42 -0800
Subject: [PATCH] fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_integrity_checker.cpp | 2 +-
src/tactic/generic_model_converter.cpp | 15 +++++++++++++++
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index d09fb9581..867dd104c 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -64,7 +64,7 @@ namespace sat {
return true;
if (c.size() == 3) {
- CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.learned()), tout << c << "\n";
+ CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.is_learned()), tout << c << "\n";
tout << "watch_list:\n";
sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
tout << "\n";);
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 485682858..2e800da48 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -53,6 +53,21 @@ void generic_model_converter::operator()(model_ref & md) {
break;
case instruction::ADD:
ev(e.m_def, val);
+ if (e.m_f->get_name() == symbol("FOX-PIT-17")) {
+ IF_VERBOSE(0, verbose_stream() << e.m_f->get_name() << " " << e.m_def << " -> " << val << "\n";);
+ ptr_vector<expr> ts;
+ ts.push_back(e.m_def);
+ while (!ts.empty()) {
+ app* t = to_app(ts.back());
+ ts.pop_back();
+ if (t->get_num_args() > 0) {
+ ts.append(t->get_num_args(), t->get_args());
+ }
+ expr_ref tmp(m);
+ ev(t, tmp);
+ IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " -> " << tmp << "\n";);
+ }
+ }
TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
arity = e.m_f->get_arity();
reset_ev = false;