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

some EA problems hit OpenSMT assertions #306

Open soonho-tri opened 8 years ago

soonho-tri commented 8 years ago 
var:
forall [-0.00001,0.00001] x1;
forall [-0.001,0.002] x2;
forall [-0.002,0.002] x3;
forall [-0.002,0.002] x4;
forall [0.00001,0.00004] s;
forall [0, 1] x1s;
forall [0, 1] x2s;
forall [0, 1] x3s;
forall [0, 1] x4s;
forall [-1, 1] cosx3;
forall [0, 1] cosx3sqr;
forall [-1, 1] sinx3;
forall [-1, 1] cosx3sinx3;
forall [-0.00000001, 1] vdot;
ctr:
(
((x1s = x1^2 and x2s = x2^2) and
((x3s = x3^2 and x4s = x4^2) and
((cosx3 = cos(x3) and cosx3sqr = cos(x3) ^ 2) and
((sinx3 = sin(x3) and cosx3sinx3 = cosx3 * sinx3)
and s=x2s+x3s+x4s))))
implies
vdot = x2*(664.68979644775390625*x1 + 156.099246978759765625*x2 - 731.9747161865234375*x3 - 76.889068603515625*x4)
- x4*(731.9747161865234375*x1 + 659.0005435943603515625*x2 - 1997.863819122314453125*x3 - 387.2728519439697265625*x4)
- (0.2*(156.099246978759765625*x1 + 413.56146717071533203125*x2 - 659.0005435943603515625*x3 - 252.9407958984375*x4)*(100.0*x1 + 194.07631769873351146316053927876*x2 - 2036.715237483512197513846331276*x3 - 393.02150737105860933695566927781*x4 - 6.0*x4s*sinx3 + 147.0*cosx3sinx3))/(3.0*cosx3sqr - 14.0)
+ ((343.0*sinx3 + 50.0*cosx3*(x1 + 2.0407631769873351146316053927876*x2 - 20.36715237483512197513846331276*x3 - 3.9302150737105860933695566927781*x4) - 5.0*x2*cosx3 - 3.0*x4s*cosx3sinx3)*(76.889068603515625*x1 + 252.9407958984375*x2 - 387.2728519439697265625*x3 - 170.12267303466796875*x4))/(3.0*cosx3sqr - 14.0)
)
;
Add Comment
$ ./dReal ~/Downloads/inp_ea.dr
unsat
Assertion failed: (initialized.find( e->getId( ) ) != initialized.end( )), function backtrackToStackSize, file /Users/soonhok/work/dreal3/src/opensmt/egraph/EgraphSolver.C, line 1123.