mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-31 11:10:42 -08:00
parent 2d0f80f78e
commit 7ada6c25d9
2 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_integrity_checker.cpp
View file

@ -64,7 +64,7 @@ namespace sat {
return true; return true;
if (c.size() == 3) { 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"; tout << "watch_list:\n";
sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0])); sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
tout << "\n";); tout << "\n";);

15
src/tactic/generic_model_converter.cpp
View file

@ -53,6 +53,21 @@ void generic_model_converter::operator()(model_ref & md) {
break; break;
case instruction::ADD: case instruction::ADD:
ev(e.m_def, val); 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";); TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
arity = e.m_f->get_arity(); arity = e.m_f->get_arity();
reset_ev = false; reset_ev = false;