Lev Nachmanson
Results
3
issues of
Lev Nachmanson
Use polarity of the non-basic variables to create bounds on basic variables in Gomory cuts
Experimenting on QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23650_edge_closing_0.smt2. The legacy solves it in seconds, the new one takes at least more than 10 minutes. In a good run legacy creates :arith-tableau-max-columns 355 :arith-tableau-max-rows 59 The...
Arithmetic