simple.t

Test verify
  $ cat - > bin/alt-ergo << EOF
  > #!/bin/sh
  > echo "2.4.0"
  > EOF

  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver

  $ bin/alt-ergo
  2.4.0

  $ bin/pyrat.py --version
  PyRAT 1.1

  $ bin/Marabou --version
  1.0.+

  $ bin/saver --version
  v1.0

  $ PATH=$(pwd)/bin:$PATH

  $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh
  > theory T
  >   use TestNetwork.NNasTuple
  >   use ieee_float.Float64
  >   use caisar.NN
  > 
  >   goal G: forall x1 x2 x3 x4 x5.
  >      (0.0:t) .< x1 .< (0.5:t) ->
  >      let (y1,_,_,_,_) = net_apply x1 x2 x3 x4 x5 in
  >      (0.0:t) .< y1 .< (0.5:t)
  > 
  >   goal H: forall x1 x2 x3 x4 x5.
  >      (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
  >      let (y1,y2,_,_,_) = net_apply x1 x2 x3 x4 x5 in
  >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
  > end
  > EOF
  Goal G: Unknown
  ()
  Goal H: Unknown
  ()