search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

Unsat result in AUV problems with "fix(dsolvers/ode_solver): skip ODE computation for trivial problem" #48

Closed danbryce closed 10 years ago

danbryce commented 10 years ago

cac5da13 is causing an issue with the auv problems when we are getting the message:

ode_solver::compute_backward: exception: Interval error: Interval Error *\ Possible division by zero.

in the --verbose output. The exception is being treated differently by this change set and causes previously sat problems to become unsat. Both auv-full.drh and auv-basic.drh illustrate the issue. I commented the lines in the change set that test return values for exceptions (i.e., ode_solver.cpp lines 391 and 436) and the unsat result went away.