alt-ergo driver: fixed incorrect syntax %% into %

de000d79 · Jean-Christophe Filliâtre · 03ba4663 · de000d79 · de000d79
Commit de000d79 authored Oct 26, 2010 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 8 additions and 2 deletions

drivers/alt_ergo.drv drivers/alt_ergo.drv +1 -1

tests/test-jcf.why tests/test-jcf.why +7 -1

No files found.
--- a/drivers/alt_ergo.drv
+++ b/drivers/alt_ergo.drv
@@ -65,7 +65,7 @@ end
 theory int.EuclideanDivision

  syntax logic div "(%1 / %2)"
-  syntax logic mod "(%1 %% %2)"
+  syntax logic mod "(%1 % %2)"

 end


--- a/tests/test-jcf.why
+++ b/tests/test-jcf.why
@@ -3,7 +3,13 @@

 theory Test

-  type t = tuple2 int int
+  use export int.Int
+
+  use real.Real as R
+  logic ( *. ) (x:real) (y:real) : real = R.(*) x y 
+
+  logic power (x : real) (n : int) : real =
+     if n = 0 then 1.0 else x *. power x (n-1)

 end