Update detection data and driver for pyrat.

config/caisar-detection-data.conf

@@ -26,7 +26,7 @@ name = "PyRAT"
 exec = "pyrat.py"
 version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
-version_ok  = "1.0"
-command = "%e %{nnet-onnx} %f"
+version_ok  = "1.1"
+command = "%e --model_path %{nnet-onnx} --property_path %f"
 driver = "caisar_drivers/pyrat.drv"
 use_at_auto_level = 1

config/drivers/pyrat.drv

 (* Why3 drivers for PyRAT *)
 
-prelude "(* This is the prelude for PyRAT *)"
-
 (* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
 valid "^Inconsistent assumption$"
 

tests/autodetect.t

@@ -15,7 +15,7 @@ Test autodetect
   2.4.0
 
   $ bin/pyrat.py --version
-  PyRAT 1.0
+  PyRAT 1.1
 
   $ bin/Marabou
   1.0.+
@@ -25,4 +25,4 @@ Test autodetect
   $ caisar config -d
   [caisar] Alt-Ergo 2.4.0
            Marabou 1.0.+
-           PyRAT 1.0
+           PyRAT 1.1

tests/bin/pyrat.py

@@ -3,11 +3,11 @@
 
 case $1 in
     --version)
-        echo "PyRAT 1.0"
+        echo "PyRAT 1.1"
         ;;
     *)
-        echo "NN: $1"
+        echo "NN: $2"
         echo "Goal:"
-        cat $2
+        cat $4
         echo "Result: Unknown"
 esac

tests/simple.t

@@ -15,7 +15,7 @@ Test verify
   2.4.0
 
   $ bin/pyrat.py --version
-  PyRAT 1.0
+  PyRAT 1.1
 
   $ bin/Marabou
   1.0.+
@@ -50,14 +50,13 @@ Test verify
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
-  <autodetect>Found prover PyRAT version 1.0, OK.
+  <autodetect>Found prover PyRAT version 1.1, OK.
   <autodetect>3 prover(s) added
   Unknown ()
   (0.00s)
   Output:
   NN: ./TestNetwork.nnet
   Goal:
-  (* This is the prelude for PyRAT *)
   0.0 <  x0
   x0 <  0.5
   0.0 <  y0
@@ -69,7 +68,6 @@ Test verify
   Output:
   NN: ./TestNetwork.nnet
   Goal:
-  (* This is the prelude for PyRAT *)
   0.0 <  x0
   x0 <  0.5
   0.5 <  x1