From f9da1d600dc2234967ded9d475c11f7599dec652 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 9 Nov 2021 14:49:26 +0100
Subject: [PATCH] Rework result rules in pyrat's driver.
---
config/drivers/pyrat.drv | 12 ++++--------
tests/bin/pyrat.py | 2 +-
tests/simple.t | 4 ++--
3 files changed, 7 insertions(+), 11 deletions(-)
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index 322a9d3a..887ff5fe 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -1,16 +1,12 @@
(* Why3 drivers for PyRAT *)
-(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
-valid "^Inconsistent assumption$"
-
-
printer "pyrat"
filename "%f-%t-%g.why"
-valid "Result: True"
-invalid "Result: False"
-timeout "Result: Timeout"
-unknown "Result: Unknown" ""
+valid "Result = [Tt]rue"
+invalid "Result = [Ff]alse"
+timeout "Result = [Tt]imeout"
+unknown "Result = [Uu]nknown" ""
transformation "inline_trivial"
transformation "introduce_premises"
diff --git a/tests/bin/pyrat.py b/tests/bin/pyrat.py
index b03e9ece..e2c01b38 100755
--- a/tests/bin/pyrat.py
+++ b/tests/bin/pyrat.py
@@ -9,5 +9,5 @@ case $1 in
echo "NN: $2"
echo "Goal:"
cat $4
- echo "Result: Unknown"
+ echo "Result = Unknown"
esac
diff --git a/tests/simple.t b/tests/simple.t
index ebab1aab..905efcc4 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -61,7 +61,7 @@ Test verify
x0 < 0.5
0.0 < y0
y0 < 0.5
- Result: Unknown
+ Result = Unknown
Unknown ()
(0.00s)
@@ -75,5 +75,5 @@ Test verify
0.0 < y0 or 0.5 < y0
0.0 < y1
y1 < 0.5
- Result: Unknown
+ Result = Unknown
--
GitLab