From 763ae0d246871446ab2413530fb9160e9e9cc4e2 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 7 Nov 2013 17:42:18 -0800 Subject: [PATCH] removed debugginf message in interpolation --- src/interp/iz3mgr.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 9ef2fa9ab..f5c7de2ad 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -489,9 +489,11 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& 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);