mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

duality abort hack and debugging hacks

Browse source
This commit is contained in:
Ken McMillan 2013-06-27 17:29:12 -07:00
parent 0eb46eef00
commit 41f77ab57c
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/interp/iz3translate_direct.cpp
View file

@ -764,7 +764,7 @@ public:
#if 1 #if 1
// std::cout << "lemma: " << ++lemma_count << "\n"; std::cout << "lemma: " << ++lemma_count << std::endl;
if(lemma_count == SHOW_LEMMA_COUNT){ if(lemma_count == SHOW_LEMMA_COUNT){
for(unsigned i = 0; i < lits.size(); i++) for(unsigned i = 0; i < lits.size(); i++)
show_lit(lits[i]); show_lit(lits[i]);
@ -786,6 +786,8 @@ public:
int sat = secondary->interpolate(preds,itps); int sat = secondary->interpolate(preds,itps);
profiling::timer_stop("foci"); profiling::timer_stop("foci");
std::cout << "lemma done" << std::endl;
// if sat, lemma isn't valid, something is wrong // if sat, lemma isn't valid, something is wrong
if(sat){ if(sat){
#if 1 #if 1
@ -1337,7 +1339,7 @@ public:
return res; return res;
} }
// #define NEW_EXTRACT_TH_LEMMA #define NEW_EXTRACT_TH_LEMMA
void get_local_hyps(const ast &proof, std::set<ast> &res){ void get_local_hyps(const ast &proof, std::set<ast> &res){
std::set<ast> hyps = get_hyps(proof); std::set<ast> hyps = get_hyps(proof);

2
src/muz_qe/duality_dl_interface.cpp
View file

@ -373,7 +373,7 @@ void dl_interface::cancel() {
#else #else
// HACK: duality can't cancel at all times, we just exit here // HACK: duality can't cancel at all times, we just exit here
std::cout << "(error \"duality canceled\")\nunknown\n"; std::cout << "(error \"duality canceled\")\nunknown\n";
exit(0); abort();
#endif #endif
} }