From a9c6c8fcf205a13c759c6f09e69b01d3b144df94 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 28 Sep 2012 15:19:53 -0700 Subject: Dafny: removed div/mod axioms, since Boogie now interprets div/mod Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support --- Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 3 --- 1 file changed, 3 deletions(-) (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index 9f22b887..c691d9da 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -231,9 +231,6 @@ namespace DafnyLanguage if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) { if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) { Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) { - // run one of the old domains - Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program); } else { // use /infer:j as the default Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true; -- cgit v1.2.3