mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Merge /home/mcmillan/pc/Code/z3_interp into interp

Browse source
This commit is contained in:
Ken McMillan 2013-05-22 13:31:24 -07:00
parent 65fbef4133 7905f48e88
commit 193e255387
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/duality/duality_solver.cpp
View file

@ -77,6 +77,7 @@ namespace Duality {
virtual void InductionFailure(RPFP::Edge *edge, const std::vector<RPFP::Node *> &children){}
virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){}
virtual void Reject(RPFP::Edge *edge, const std::vector<RPFP::Node *> &Children){}
virtual void Message(const std::string &msg){}
virtual ~Reporter(){}
};
@ -1154,7 +1155,7 @@ namespace Duality {
}
#endif
if(!full_scan && candidates.empty()){
std::cout << "No candidates from updates. Trying full scan.\n";
reporter->Message("No candidates from updates. Trying full scan.");
GenCandidatesFromInductionFailure(true);
}
}
@ -2193,6 +2194,9 @@ namespace Duality {
s << " " << children[i]->number;
s << std::endl;
}
virtual void Message(const std::string &msg){
ev(); s << "msg " << msg << std::endl;
}
};