From de000d79d891e0c656d6b61b2971dd8bcc569dc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Christophe=20Filli=C3=A2tre?= <filliatr@lri.fr>
Date: Tue, 26 Oct 2010 07:01:56 +0000
Subject: [PATCH] alt-ergo driver: fixed incorrect syntax %% into %

---
 drivers/alt_ergo.drv | 2 +-
 tests/test-jcf.why   | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/drivers/alt_ergo.drv b/drivers/alt_ergo.drv
index 1b078e349..c192132d6 100644
--- 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
 
diff --git a/tests/test-jcf.why b/tests/test-jcf.why
index acf0d16a9..dca151887 100644
--- 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
 
-- 
GitLab