Test verify $ cat - > bin/alt-ergo << EOF > #!/bin/sh > echo "2.4.0" > EOF $ cat - > test_data.csv << EOF > # 1 3 > 1,0.5,0.5,0.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=SAVer --dataset-csv=test_data.csv - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/' > theory T > use TestSVM.SVMasArray > use ieee_float.Float64 > use caisar.SVM > > goal G: forall a : input_type. > robust_to svm_apply a (8.0:t) > end > EOF <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1 <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1 <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1 <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1 <autodetect>0 prover(s) added <autodetect>Generating strategies: <autodetect>Found prover Alt-Ergo version 2.4.0, OK. <autodetect>Found prover Marabou version 1.0.+, OK. <autodetect>Found prover PyRAT version 1.1, OK. <autodetect>Found prover SAVer version v1.0, OK. <autodetect>4 prover(s) added Goal G: High failure