Merge

2 files changed, 7 insertions, 8 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ca526173..53e8e86a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -613,15 +613,15 @@ var $Tick: TickType;
 // -- Arithmetic -------------------------------------------------

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

 

-// the connection between % and /

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

+// the connection between mod and div

+axiom (forall x:int, y:int :: {x mod y} {x div y}  x mod y == x - x div 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);

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

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

 

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

+// the following axiom has some unfortunate matching, but it does state a property about mod 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);

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

 

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

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)