diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 0787588c4e8ec2c8a672af8974a9b1c443e4638f..01366e62061861ba464e80f75a6b648a9f06c33d 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -50,13 +50,14 @@ let create_new_nn env input_vars outputs : string =
let get_input =
Why3.Term.Hls.memo 10 (fun ls ->
let i = Why3.Term.Mls.find_exn UnknownLogicSymbol ls input_vars in
- IR.Node.create (Gather { input; data = i }))
+ Ir.Nier_simple.Node.gather_int input i)
in
let rec convert_old_nn (old_nn : Language.nn) old_index old_nn_args :
IR.GFloat.Node.t =
let old_index = Why3.Number.to_small_integer old_index in
let input () =
- IR.Node.create (Concat { inputs = List.map ~f:convert_term old_nn_args })
+ IR.Node.create
+ (Concat { inputs = List.map ~f:convert_term old_nn_args; axis = 0 })
in
let old_nn =
match Onnx.Simple.parse old_nn.nn_filename with
@@ -69,7 +70,7 @@ let create_new_nn env input_vars outputs : string =
| Ok { nier = Ok g; _ } -> g
in
let out = IR.Node.replace_input input (IR.output old_nn) in
- IR.Node.create (Gather { input = out; data = old_index })
+ Ir.Nier_simple.Node.gather_int out old_index
and convert_term term : IR.GFloat.Node.t =
if not (Why3.Ty.ty_equal (Option.value_exn term.Why3.Term.t_ty) th_f64.ty)
then
@@ -79,15 +80,18 @@ let create_new_nn env input_vars outputs : string =
| Tconst (Why3.Constant.ConstReal r) ->
IR.Node.create
(Constant
- { data = IR.Tensor.create_1_float @@ Utils.float_of_real_constant r })
+ {
+ data =
+ IR.GenTensor.create_1_float @@ Utils.float_of_real_constant r;
+ })
| Tapp (ls, []) -> get_input ls
- | Tapp (ls, [ a; b ]) when Why3.Term.ls_equal ls th_f64.add ->
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.add ->
IR.Node.create (Add { input1 = convert_term a; input2 = convert_term b })
- | Tapp (ls, [ a; b ]) when Why3.Term.ls_equal ls th_f64.sub ->
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.sub ->
IR.Node.create (Sub { input1 = convert_term a; input2 = convert_term b })
- | Tapp (ls, [ a; b ]) when Why3.Term.ls_equal ls th_f64.mul ->
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.mul ->
IR.Node.create (Mul { input1 = convert_term a; input2 = convert_term b })
- | Tapp (ls, [ a; b ]) when Why3.Term.ls_equal ls th_f64.div ->
+ | Tapp (ls, [ _; a; b ]) when Why3.Term.ls_equal ls th_f64.div ->
IR.Node.create (Div { input1 = convert_term a; input2 = convert_term b })
| Tapp (ls, [ a ]) when Why3.Term.ls_equal ls th_f64.neg ->
IR.Node.create
@@ -96,7 +100,7 @@ let create_new_nn env input_vars outputs : string =
input1 = convert_term a;
input2 =
IR.Node.create
- (Constant { data = IR.Tensor.create_1_float (-1.) });
+ (Constant { data = IR.GenTensor.create_1_float (-1.) });
})
| Tapp
( ls_get (* [ ] *),
@@ -135,21 +139,26 @@ let create_new_nn env input_vars outputs : string =
| Tbinop (_, _, _)
| Tcase (_, _)
| Tnot _ | Ttrue | Tfalse ->
- Logging.not_implemented_yet (fun fmt -> fmt "Why3 term to IR")
+ Logging.not_implemented_yet (fun m ->
+ m "Why3 term to IR: %a" Why3.Pretty.print_term term)
| Tvar _ | Teps _ | Tquant (_, _) ->
- Logging.user_error (fun fmt -> fmt "unimplementable: why3 term to IR")
+ Logging.not_implemented_yet (fun m ->
+ m "Why3 term to IR (impossible?): %a" Why3.Pretty.print_term term)
in
- let r = ref (-1) in
- let inputs =
+ let r = ref (List.length outputs) in
+ let outputs =
List.rev_map outputs ~f:(fun o ->
- Int.incr r;
+ Int.decr r;
assert (!r = o.new_index);
convert_old_nn o.old_nn o.old_index o.old_nn_args)
in
- let outputs = IR.Node.create (Concat { inputs }) in
+ let outputs = IR.Node.create (Concat { inputs = outputs; axis = 0 }) in
let nn = IR.create outputs in
- let filename = Stdlib.Filename.temp_file "caisar" ".onnx" in
+ let filename =
+ Stdlib.Filename.temp_file ~temp_dir:"/home/bobot/tmp/caisar/" "caisar"
+ ".onnx"
+ in
Onnx.Simple.write nn filename;
filename
@@ -253,7 +262,7 @@ let abstract_nn_term env =
create_new_nn env input_vars (List.map ~f:fst output_vars)
in
let task =
- Why3.Task.add_meta task Meta.meta_output [ MAstr nn_filename ]
+ Why3.Task.add_meta task Meta.meta_nn_filename [ MAstr nn_filename ]
in
(acc, Why3.Task.add_decl task decl)
| Decl { d_node = Dprop (_, _, _); _ } ->
diff --git a/tests/acasxu.t b/tests/acasxu.t
index 01f4e1db673a0f0e2ef9312dda4e99ecedc73e1d..5ac9f85712bc9b97771b5dee7ded54726603e8f1 100644
--- a/tests/acasxu.t
+++ b/tests/acasxu.t
@@ -12,7 +12,7 @@ Test verify on acasxu
> use caisar.model.Model
> use caisar.model.NN
>
- > let constant nn: model nn = read_model "TestNetwork.nnet"
+ > let constant nn: model nn = read_model "../examples/acasxu/nets/onnx/ACASXU_1_1.onnx"
>
> type input = vector t
>
@@ -89,6 +89,16 @@ Test verify on acasxu
> let o = (nn@@i)[clear_of_conflict] in
> (denormalize_output o)
>
+ > let run2 (j:input)
+ > requires { has_length j 5 }
+ > requires { valid_input j }
+ > requires { intruder_distant_and_slow j }
+ > ensures { result } =
+ > let i = normalize_input j in
+ > let o1 = (nn@@i)[clear_of_conflict] in
+ > let o2 = (nn@@i)[clear_of_conflict] in
+ > o1 .= o2
+ >
> (* goal P1:
> forall i: input.
> has_length i 5 ->
@@ -139,7 +149,110 @@ Test verify on acasxu
le
(add RNE
(mul RNE
- (nn_nnet
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x1 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x2 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
+ [0] (373.9499200000000200816430151462554931640625:t))
+ (7.51888402010059753166615337249822914600372314453125:t))
+ (1500.0:t)
+ nn_onnx,
+ (Interpreter_types.Model
+ (Interpreter_types.ONNX, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ nn_ty_elt = t;
+ nn_filename =
+ "./../examples/acasxu/nets/onnx/ACASXU_1_1.onnx";
+ nn_format = <nier> }))
+ vector,
+ 5
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ 0.0 <= x3
+ x3 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x4
+ x4 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x5
+ x5 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x6
+ x6 <= 1200.0
+ 0.0 <= x7
+ x7 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x3
+ 1145.0 <= x6
+ x7 <= 60.0
+ y0 <= 3.991125645861615112153231166303157806396484375
+
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'run2'vc':
+ forall x:t, x1:t, x2:t, x3:t, x4:t.
+ ((le (0.0:t) x /\ le x (60760.0:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x1 /\
+ le x1 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x2 /\
+ le x2 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (100.0:t) x3 /\ le x3 (1200.0:t)) /\ le (0.0:t) x4 /\ le x4 (1200.0:t)) /\
+ le (55947.6909999999988940544426441192626953125:t) x /\
+ le (1145.0:t) x3 /\ le x4 (60.0:t) ->
+ eq
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x1 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x2 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
+ [0]
+ (nn_onnx
+ @@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
+ (div RNE (sub RNE x1 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x2 (0.0:t))
+ (6.2831853071800001231395071954466402530670166015625:t))
+ (div RNE (sub RNE x3 (650.0:t)) (1100.0:t))
+ (div RNE (sub RNE x4 (600.0:t)) (1200.0:t)))
+ [0]
+ nn_onnx,
+ (Interpreter_types.Model
+ (Interpreter_types.ONNX, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ nn_ty_elt = t;
+ nn_filename =
+ "./../examples/acasxu/nets/onnx/ACASXU_1_1.onnx";
+ nn_format = <nier> }))
+ vector,
+ 5
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ 0.0 <= x3
+ x3 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x4
+ x4 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x5
+ x5 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x6
+ x6 <= 1200.0
+ 0.0 <= x7
+ x7 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x3
+ 1145.0 <= x6
+ x7 <= 60.0
+
+
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'test'vc':
+ forall x:t, x1:t, x2:t, x3:t, x4:t.
+ ((le (0.0:t) x /\ le x (60760.0:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x1 /\
+ le x1 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t)) x2 /\
+ le x2 (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (100.0:t) x3 /\ le x3 (1200.0:t)) /\ le (0.0:t) x4 /\ le x4 (1200.0:t)) /\
+ le (55947.6909999999988940544426441192626953125:t) x /\
+ le (1145.0:t) x3 /\ le x4 (60.0:t) ->
+ le
+ (add RNE
+ (mul RNE
+ (nn_onnx
@@ vector (div RNE (sub RNE x (19791.0:t)) (60261.0:t))
(div RNE (sub RNE x1 (0.0:t))
(6.2831853071800001231395071954466402530670166015625:t))
@@ -150,24 +263,252 @@ Test verify on acasxu
[0] (373.9499200000000200816430151462554931640625:t))
(7.51888402010059753166615337249822914600372314453125:t))
(1500.0:t)
- nn_nnet,
+ nn_onnx,
+ (Interpreter_types.Model
+ (Interpreter_types.ONNX, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ nn_ty_elt = t;
+ nn_filename =
+ "./../examples/acasxu/nets/onnx/ACASXU_1_1.onnx";
+ nn_format = <nier> }))
+ vector,
+ 5
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ 0.0 <= x3
+ x3 <= 60760.0
+ -3.141592653589793115997963468544185161590576171875 <= x4
+ x4 <= 3.141592653589793115997963468544185161590576171875
+ -3.141592653589793115997963468544185161590576171875 <= x5
+ x5 <= 3.141592653589793115997963468544185161590576171875
+ 100.0 <= x6
+ x6 <= 1200.0
+ 0.0 <= x7
+ x7 <= 1200.0
+ 55947.6909999999988940544426441192626953125 <= x3
+ 1145.0 <= x6
+ x7 <= 60.0
+ y0 <= 3.991125645861615112153231166303157806396484375
+
+ [DEBUG]{InterpretGoal} Interpreted formula for goal 'P3':
+ forall x:t, x1:t, x2:t, x3:t, x4:t.
+ ((le (0.0:t) (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t))
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (neg (3.141592653589793115997963468544185161590576171875:t))
+ (add RNE
+ (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (3.141592653589793115997963468544185161590576171875:t)) /\
+ (le (100.0:t) (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) /\
+ le (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
+ le (0.0:t) (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) /\
+ le (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
+ ((le (1500.0:t) (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) /\
+ le (add RNE (mul RNE x (60261.0:t)) (19791.0:t)) (1800.0:t)) /\
+ le (neg (0.059999999999999997779553950749686919152736663818359375:t))
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le
+ (add RNE
+ (mul RNE x1 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t))
+ (0.059999999999999997779553950749686919152736663818359375:t)) /\
+ le (3.100000000000000088817841970012523233890533447265625:t)
+ (add RNE
+ (mul RNE x2 (6.2831853071800001231395071954466402530670166015625:t))
+ (0.0:t)) /\
+ le (980.0:t) (add RNE (mul RNE x3 (1100.0:t)) (650.0:t)) /\
+ le (960.0:t) (add RNE (mul RNE x4 (1200.0:t)) (600.0:t)) ->
+ not (((lt (nn_onnx @@ vector x x1 x2 x3 x4)[0]
+ (nn_onnx @@ vector x x1 x2 x3 x4)[1] /\
+ lt (nn_onnx @@ vector x x1 x2 x3 x4)[0]
+ (nn_onnx @@ vector x x1 x2 x3 x4)[2]) /\
+ lt (nn_onnx @@ vector x x1 x2 x3 x4)[0]
+ (nn_onnx @@ vector x x1 x2 x3 x4)[3]) /\
+ lt (nn_onnx @@ vector x x1 x2 x3 x4)[0]
+ (nn_onnx @@ vector x x1 x2 x3 x4)[4])
+ nn_onnx,
(Interpreter_types.Model
- (Interpreter_types.NNet, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
+ (Interpreter_types.ONNX, { Language.nn_nb_inputs = 5; nn_nb_outputs = 5;
nn_ty_elt = t;
- nn_filename = "./TestNetwork.nnet";
- nn_format = Language.NNet }))
+ nn_filename =
+ "./../examples/acasxu/nets/onnx/ACASXU_1_1.onnx";
+ nn_format = <nier> }))
vector,
5
- [ERROR]{NN-Gen} No parsed NN for './TestNetwork.nnet': Cannot read protobuf
- Unrecoverable error: please report the issue at
- https://git.frama-c.com/pub/caisar/issues
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ -0.328421367053318091766556108268559910356998443603515625 <= x0
+ x0 <= 0.67985927880386987087746319957659579813480377197265625
+ -0.499999999999967081887319864108576439321041107177734375 <= x1
+ x1 <= 0.499999999999967081887319864108576439321041107177734375
+ -0.499999999999967081887319864108576439321041107177734375 <= x2
+ x2 <= 0.499999999999967081887319864108576439321041107177734375
+ -0.5 <= x3
+ x3 <= 0.5
+ -0.5 <= x4
+ x4 <= 0.5
+ -0.303529646039727207806890874053351581096649169921875 <= x0
+ x0 <= -0.298551301837009008810497334707179106771945953369140625
+ -0.0095492965855130916563719978285007528029382228851318359375 <= x1
+ x1 <= 0.0095492965855130916563719978285007528029382228851318359375
+ 0.493380323584843072382000173092819750308990478515625 <= x2
+ 0.299999999999999988897769753748434595763683319091796875 <= x3
+ 0.299999999999999988897769753748434595763683319091796875 <= x4
+ (((y0 >= y1 or y0 >= y2) or y0 >= y3) or y0 >= y4)
+
+ Goal run'vc: Unknown ()
+ Goal run2'vc: Unknown ()
+ Goal test'vc: Unknown ()
+ Goal P3: Unknown ()
$ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw
- [ERROR]{NN-Gen} No parsed NN for './TestNetwork.nnet': Cannot read protobuf
- Unrecoverable error: please report the issue at
- https://git.frama-c.com/pub/caisar/issues
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ ;;; produced by PyRAT/VNN-LIB driver
+ ;;; produced by VNN-LIB driver
+ ;; X_0
+ (declare-const X_0 Real)
+
+ ;; X_1
+ (declare-const X_1 Real)
+
+ ;; X_2
+ (declare-const X_2 Real)
+
+ ;; X_3
+ (declare-const X_3 Real)
+
+ ;; X_4
+ (declare-const X_4 Real)
+
+ ;; X_5
+ (declare-const X_5 Real)
+
+ ;; X_6
+ (declare-const X_6 Real)
+
+ ;; X_7
+ (declare-const X_7 Real)
+
+ ;; Requires
+ (assert (>= X_3 0.0))
+ (assert (<= X_3 60760.0))
+ (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_6 100.0))
+ (assert (<= X_6 1200.0))
+ (assert (>= X_7 0.0))
+ (assert (<= X_7 1200.0))
+
+ ;; Requires
+ (assert (>= X_3 55947.6909999999988940544426441192626953125))
+ (assert (>= X_6 1145.0))
+ (assert (<= X_7 60.0))
+
+ ;; Y_0
+ (declare-const Y_0 Real)
+
+ ;; Goal run'vc
+ (assert (>= Y_0 3.991125645861615112153231166303157806396484375))
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ ;;; produced by PyRAT/VNN-LIB driver
+ ;;; produced by VNN-LIB driver
+ ;; X_0
+ (declare-const X_0 Real)
+
+ ;; X_1
+ (declare-const X_1 Real)
+
+ ;; X_2
+ (declare-const X_2 Real)
+
+ ;; X_3
+ (declare-const X_3 Real)
+
+ ;; X_4
+ (declare-const X_4 Real)
+
+ ;; X_5
+ (declare-const X_5 Real)
+
+ ;; X_6
+ (declare-const X_6 Real)
+
+ ;; X_7
+ (declare-const X_7 Real)
+
+ ;; Requires
+ (assert (>= X_3 0.0))
+ (assert (<= X_3 60760.0))
+ (assert (>= X_4 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_4 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_5 -3.141592653589793115997963468544185161590576171875))
+ (assert (<= X_5 3.141592653589793115997963468544185161590576171875))
+ (assert (>= X_6 100.0))
+ (assert (<= X_6 1200.0))
+ (assert (>= X_7 0.0))
+ (assert (<= X_7 1200.0))
+
+ ;; Requires
+ (assert (>= X_3 55947.6909999999988940544426441192626953125))
+ (assert (>= X_6 1145.0))
+ (assert (<= X_7 60.0))
+
+ ;; Y_1
+ (declare-const Y_1 Real)
+
+ ;; Y_0
+ (declare-const Y_0 Real)
+
+ [ERROR] This expression isn't supported:
+ eq y y1
+ VNN-LIB: cannot negate term
$ caisar verify --prover Marabou --ltag=ProverSpec file.mlw
- [ERROR]{NN-Gen} No parsed NN for './TestNetwork.nnet': Cannot read protobuf
- Unrecoverable error: please report the issue at
- https://git.frama-c.com/pub/caisar/issues
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x3 >= 0.0
+ x3 <= 60760.0
+ x4 >= -3.141592653589793115997963468544185161590576171875
+ x4 <= 3.141592653589793115997963468544185161590576171875
+ x5 >= -3.141592653589793115997963468544185161590576171875
+ x5 <= 3.141592653589793115997963468544185161590576171875
+ x6 >= 100.0
+ x6 <= 1200.0
+ x7 >= 0.0
+ x7 <= 1200.0
+ x3 >= 55947.6909999999988940544426441192626953125
+ x6 >= 1145.0
+ x7 <= 60.0
+ y0 >= 3.991125645861615112153231166303157806396484375
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x3 >= 0.0
+ x3 <= 60760.0
+ x4 >= -3.141592653589793115997963468544185161590576171875
+ x4 <= 3.141592653589793115997963468544185161590576171875
+ x5 >= -3.141592653589793115997963468544185161590576171875
+ x5 <= 3.141592653589793115997963468544185161590576171875
+ x6 >= 100.0
+ x6 <= 1200.0
+ x7 >= 0.0
+ x7 <= 1200.0
+ x3 >= 55947.6909999999988940544426441192626953125
+ x6 >= 1145.0
+ x7 <= 60.0
+ [ERROR] This expression isn't supported:
+ eq y y1
+ Marabou: cannot negate term