From 589053fc102e9a7a38c497defc75a96f782489d2 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 27 Oct 2015 18:27:25 -0700 Subject: [PATCH] interp: fix gomory cut rule with non-local conclusion (issue #200) --- src/interp/iz3translate.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 51084f809..5bb91a49e 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1201,9 +1201,12 @@ public: ast t = arg(my_con,0); ast c = arg(my_con,1); ast d = gcd_of_coefficients(t); + /* t = z3_simplify(mk_idiv(t,d)); c = z3_simplify(mk_idiv(c,d)); ast cut_con = make(op(my_con),t,c); + */ + ast cut_con = con; return iproof->make_cut_rule(my_con,d,cut_con,res); }