Merge

3 files changed, 19 insertions, 40 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index e6d05bea..fafc9484 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -647,18 +647,3 @@ type TickType;
 var $Tick: TickType;

 

 // ---------------------------------------------------------------

-// -- Arithmetic -------------------------------------------------

-// ---------------------------------------------------------------

-

-// the connection between % and /

-axiom (forall x:int, y:int :: {x % y} {x / y}  x % y == x - x / y * y);

-

-// remainder is always Euclidean Modulus.

-axiom (forall x:int, y:int :: {x % y}  0 < y  ==>  0 <= x % y  &&  x % y < y);

-axiom (forall x:int, y:int :: {x % y}  y < 0  ==>  0 <= x % y  &&  x % y < -y);

-

-// the following axiom has some unfortunate matching, but it does state a property about % that

-// is sometimes useful

-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b  ==>  a + d <= b);

-

-// ---------------------------------------------------------------

diff --git a/Binaries/PrepareBoogieZip.bat b/Binaries/PrepareBoogieZip.bat
index 9edeec4a..1f64a31c 100644
--- a/Binaries/PrepareBoogieZip.bat
+++ b/Binaries/PrepareBoogieZip.bat
@@ -7,33 +7,28 @@ if exist %DEST_DIR% del /q %DEST_DIR%\*
 if not exist %DEST_DIR% mkdir %DEST_DIR%
 
 for %%f in (
-  AbsInt.dll                  AbsInt.pdb
-  AIFramework.dll             AIFramework.pdb
-  Basetypes.dll               Basetypes.pdb
-  Boogie.exe                  Boogie.pdb
-  BVD.exe                     BVD.pdb
-  CodeContractsExtender.dll   CodeContractsExtender.pdb
-  Core.dll                    Core.pdb
-  Dafny.exe                   Dafny.pdb
-  DafnyPipeline.dll           DafnyPipeline.pdb
-  Graph.dll                   Graph.pdb
-  Houdini.dll                 Houdini.pdb
-  Model.dll                   Model.pdb
-  ParserHelper.dll            ParserHelper.pdb
-  Provers.Isabelle.dll        Provers.Isabelle.pdb
-  Provers.Simplify.dll        Provers.Simplify.pdb
-  Provers.SMTLib.dll          Provers.SMTLib.pdb
-  Provers.TPTP.dll            Provers.TPTP.pdb
-  Provers.Z3.dll              Provers.Z3.pdb
-  VCExpr.dll                  VCExpr.pdb
-  VCGeneration.dll            VCGeneration.pdb
-  DafnyPrelude.bpl
-  DafnyRuntime.cs
+  AbsInt.dll                          AbsInt.pdb
+  Basetypes.dll                       Basetypes.pdb
+  Boogie.exe                          Boogie.pdb
+  CodeContractsExtender.dll           CodeContractsExtender.pdb
+  Core.dll                            Core.pdb
+  Dafny.exe                           Dafny.pdb
+  DafnyPrelude.bpl                    DafnyRuntime.cs
+  DafnyPipeline.dll                   DafnyPipeline.pdb
+  Graph.dll                           Graph.pdb
+  Houdini.dll
+  Model.dll                           Model.pdb
+  ParserHelper.dll                    ParserHelper.pdb
+  Provers.SMTLib.dll                  Provers.SMTLib.pdb
   TypedUnivBackPred2.sx
-  UnivBackPred2.smt2
+  UnivBackPred2.smt                   UnivBackPred2.smt2
   UnivBackPred2.sx
+  VCExpr.dll                          VCExpr.pdb
+  VCGeneration.dll                    VCGeneration.pdb
 ) do (
   copy %%f %DEST_DIR%
 )
 
+xcopy /E /I /Y CodeContracts "%DEST_DIR%/CodeContracts"
+
 echo Done.  Now, manually put the contents of the %DEST_DIR% directory into Boogie.zip
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
index d3e3777f..9bb05bfb 100644
--- a/Binaries/UnivBackPred2.smt2
+++ b/Binaries/UnivBackPred2.smt2
@@ -3,7 +3,6 @@
 (set-info :category "industrial")

 (declare-sort |T@U| 0)

 (declare-sort |T@T| 0)

-(declare-fun int_div (Int Int) Int)

-(declare-fun int_mod (Int Int) Int)

+(declare-fun real_pow (Real Real) Real)

 (declare-fun UOrdering2 (|T@U| |T@U|) Bool)

 (declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)