search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

CAPD4 bug? #169

Closed soonhokong closed 9 years ago

soonhokong commented 9 years ago

Reproduce Step

========== CAPD STRING ==========
var:x1_2_0, x2_2_0, tau_2_0;fun:-(5+((-1)*((0.5*(19.613299999999998846078597125597^(0.5)))*(x1_2_0^(0.5)))))/2, -((0.5*(19.613299999999998846078597125597^(0.5)))*((x1_2_0^(0.5))+((-1)*(x2_2_0^(0.5)))))/4, -1;
========== Initial Condition ==========
X_0 : {[2.67942,5],[5.16944,9.89842],[0,0]}
X_t : {[3.10689,5],[4.65776,5],[1,1]}
T   : [0.980469,1]

Output From CAPD

terminate called after throwing an instance of 'std::runtime_error'
  what():  capd::diffAlgebra::Curve::operator() error - empty intersection. Report this error to CAPD developers!

It seems that it hits https://github.com/dreal-deps/capdDynSys-4.0/blob/master/capdDynSys4/include/capd/diffAlgebra/Curve.hpp#L93-L94

soonhokong commented 9 years ago

It occurs while solving https://github.com/dreal/dreal3/blob/master/src/tests/nra_ode/water-double_3.smt2, at a backward ODE pruning step.

It's only reproducible on a linux machine, not on a mac.