Closed chrjabs closed 6 months ago
Thanks for the fix. I copied it to our Internal repo ans merged it there. Should be displayed soonish!
The assertion fail on this instance while certifying with rational arithmetic should be resolved already. We are running some tests to exclude further errors. Thanks for reporting this.
The float constant
INFINITY
cannot be converted to theRational
type, which leads to a runtime error when attempting to compare coefficients withINFINITY
, as seen below. The instance used is available in the RoundingSAT repository.