-timeLimit ignored when -errorLimit specified

that pretty much says it all

Id #10247 | Release: None | Updated: Feb 25, 2015 at 9:53 PM by nimrodpar | Created: Feb 25, 2015 at 9:53 PM by nimrodpar

Dependence of libraries on CommandLineOptions.Clo should be removed

I'm currently using Boogie as a library and there is an issue that makes it incredibly painful to use. The issue is lots of the code refers to CommandLineOptions.Clo which is the global command lin...

Id #10244 | Release: None | Updated: Oct 21, 2014 at 12:40 PM by danliew | Created: Oct 21, 2014 at 12:40 PM by danliew

Doomed tests need to be enabled and fixed

The tests in Test/doomed are really broken. If the lit.local.cfg is removed (this is preventing them from being executed) then they hang! Some .bpl files in that directory aren't use either. They...

Id #10243 | Release: None | Updated: Sep 21, 2014 at 10:21 PM by danliew | Created: Sep 21, 2014 at 10:21 PM by danliew

AbsHoudini tests need to be enabled and fixed

The tests in Test/AbsHoudini are currently disabled because some of them are broken. This is bad because we aren't tracking regressions introduced for this feature. UNRESOLVED: Boogie :: AbsHoudini...

Id #10242 | Release: None | Updated: Sep 21, 2014 at 9:56 PM by danliew | Created: Sep 21, 2014 at 9:56 PM by danliew

Problem using return value in ensures code expression.

The current version of Boogie ("version 2.2.30705.1126") from Codeplex without any command line flags falsely reports an error on the following program. procedure p() returns ($r: int) ensures |{...

Id #10241 | Release: None | Updated: Aug 7, 2014 at 7:45 PM by mje | Created: Jul 31, 2014 at 4:24 PM by mje

Boogie file passes type checker but crashes

I've generated a Boogie file that passes the type checker but crashes Boogie with a violated assertion. Certainly, there is a bug in the generated file, but maybe it should not crash Booige.

Id #10237 | Release: None | Updated: May 8, 2013 at 2:42 AM by schaef | Created: May 8, 2013 at 2:42 AM by schaef

BVD Crashes w/ Model Generated by Dafny

Hello, The Boogie Verification Debugger (BVD) crashes with an example model file that was generated by Dafny. I've attached the input Dafny file. The version of Dafny I used was: Dafny program...

Id #10236 | Release: None | Updated: Apr 2, 2013 at 1:57 AM by jaltidor | Created: Apr 2, 2013 at 1:52 AM by jaltidor

Crash running Boogie ...

Hi... Just started playing with Boogie after installing as oppose to using the rise4fun website..... I ended up crashing it by removing an assert in the quicksort example on the website Here ...

Id #10235 | Release: None | Updated: Mar 5, 2013 at 11:19 PM by bmellow | Created: Mar 5, 2013 at 11:17 PM by bmellow

[Boogie] 2 bugs using reals in boogie

Hi, first of all thank you very much for adding support for real values to Boogie. Unfortunately there are two bugs, when using reals in a Boogie file: First: Boogie and BVD are not able to p...

Id #10234 | Release: None | Updated: Nov 21, 2012 at 6:16 PM by reicherdt | Created: Nov 21, 2012 at 6:16 PM by reicherdt

[BVD] bug in command line processing

Hi, there is a small bug in the processing of command line arguments in BVD. When using a full path of a model file including the drive letter, BVD splits the path on the ":" of "C:...". The ...

Id #10233 | Release: None | Updated: Nov 21, 2012 at 5:53 PM by reicherdt | Created: Nov 21, 2012 at 5:53 PM by reicherdt