Rework result rules in pyrat's driver.

config/drivers/pyrat.drv

 (* 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"

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

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