[Marabou] Introduce the used symbol in the initial task

src/transformations/vars_on_lhs.ml

@@ -7,6 +7,7 @@
 let make_rt env =
   let open Why3 in
   let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+  let t = Theory.ns_find_ts th.th_export [ "t" ] in
   let le = Theory.ns_find_ls th.th_export [ "le" ] in
   let lt = Theory.ns_find_ls th.th_export [ "lt" ] in
   let ge = Theory.ns_find_ls th.th_export [ "ge" ] in
@@ -32,11 +33,17 @@ let make_rt env =
       else t
     | _ -> t
   in
-  rt
+  let init = None in
+  let init = Task.add_ty_decl init t in
+  let init = Task.add_param_decl init le in
+  let init = Task.add_param_decl init lt in
+  let init = Task.add_param_decl init ge in
+  let init = Task.add_param_decl init gt in
+  (rt, init)
 
 let vars_on_lhs env =
-  let rt = make_rt env in
-  Why3.Trans.rewrite rt None
+  let rt, init = make_rt env in
+  Why3.Trans.rewrite rt init
 
 let init () =
   Why3.Trans.register_env_transform

tests/marabout.t

+Test verify
+  $ cat - > bin/alt-ergo << EOF
+  > #!/bin/sh
+  > echo "2.4.0"
+  > EOF
+
+  $ cat - > bin/Marabou << EOF
+  > #!/bin/sh
+  > echo "1.0.+"
+  > EOF
+
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou
+
+  $ bin/alt-ergo
+  2.4.0
+
+  $ bin/pyrat.py --version
+  PyRAT 1.1
+
+  $ bin/Marabou
+  1.0.+
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ caisar verify -L . --format whyml --prover=Marabou - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
+  > theory T
+  >   use TestNetwork.AsTuple
+  >   use ieee_float.Float64
+  >   use caisar.NNet
+  > 
+  >   goal G: forall x1 x2 x3 x4 x5.
+  >      (0.0:t) .< x1 .< (0.5:t) ->
+  >      let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
+  >      (0.0:t) .< y1 .< (0.5:t)
+  > end
+  > EOF
+  <autodetect>0 prover(s) added
+  <autodetect>Generating strategies:
+  <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
+  <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <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.1, OK.
+  <autodetect>3 prover(s) added
+  HERE: lt (0.0:t) x1!
+  HERE: lt (0.0:t) y!
+  Goal G: High failure
+  Output:
+  1.0.+
+