diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv index 322a9d3a7217f51880b27ae84937857a3b309afe..887ff5feefbf2e5ae34745fbc2152e52fc051a25 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 b03e9ecea79b8b2d4226b6d820bed954f9411cb7..e2c01b3822a1f3c39400f3df74fbe7eee2b29951 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 ebab1aaba97b815c4c2b5198b52dff1ce033f932..905efcc4e725d2f1ba9e2332da3103c9539061a9 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