search

dreal / dreal2

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

Uncaught exception returned by dReach #5

Closed rachelwang closed 10 years ago

rachelwang commented 10 years ago 
Uncaught exception: Bmc.SMTException("time should be defined once and only once.")

For the drh files, you can go to https://github.com/rachelwang/statsmt_sq/tree/master/models. Both the "gear_shift_auto.pdrh", and "queuing_system.pdrh" report this error.

soonhokong commented 10 years ago 
Uncaught exception: Bmc.SMTException("time should be defined once and only once.")

It means that either you haven't defined time variable in your .drh file or you defined it more than twice. In your example gear_shift_auto.pdrh, you didn't define time variable.

Please specify the way to reproduce the error next time. If you paste the generated .drh or smt2 to gist and link them to your issue, that would be very helpful for me to work on them.

rachelwang commented 10 years ago

I declared "t" instead of "time"...

What is silly mistake!

Thanks!

On Apr 16, 2014, at 2:06 PM, Soonho Kong notifications@github.com wrote:

''' Uncaught exception: Bmc.SMTException("time should be defined once and only once.") '''

It means that either you haven't defined time variable in your .drh file or you defined it more than twice. In your example gear_shift_auto.pdrh, you didn't define time variable.

Please specify the way to reproduce the error next time. If you paste the generated .drh or smt2 to gist and link them to your issue, that would be very helpful for me to work on them.

— Reply to this email directly or view it on GitHub.

soonhokong commented 10 years ago

The problem is that it's not really well-documented. We should have one.