mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity

removed debugginf message in interpolation

Browse source
This commit is contained in:
Ken McMillan 2013-11-07 17:42:18 -08:00
parent a898bad961
commit 763ae0d246
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/interp/iz3mgr.cpp
View file

@ -489,9 +489,11 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-2);
#if 0
if(num_prems(proof) < numps-2){
std::cout << "bad farkas rule: " << num_prems(proof) << " premises should be " << numps-2 << "\n";
}
#endif
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);