simple_ovo.t

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