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 ()