search

schillic / dreal

dReal: An SMT Solver for Nonlinear Theories of the Reals
http://dreal.cs.cmu.edu
GNU General Public License v3.0
0 stars 0 forks source link

correctly respect the time interval in SpaceEx #2

Closed schillic closed 7 years ago

schillic commented 9 years ago

Let T = [l, r] be the time interval for a call to the ODE solver. The intention is to return the reachable states for time interval [l, r]. Currently we return the reachable states from SpaceEx for time interval [0, r], which is an (unnecessary) overapproximation.