diff --git a/stdlib/dune b/stdlib/dune
index 46fd7c7306e71bd60e4acd523f4e3ea31a29366e..fd72e779d0eb3ec5c7d005e1eee2fbd4424906c3 100644
--- a/stdlib/dune
+++ b/stdlib/dune
@@ -2,5 +2,5 @@
  (section
   (site
    (caisar stdlib)))
- (files caisar.mlw robustness.mlw vector.mlw nn.mlw dataset.mlw)
+ (files caisar.mlw robust.mlw vector.mlw nn.mlw dataset.mlw)
  (package caisar))
diff --git a/stdlib/robustness.mlw b/stdlib/robust.mlw
similarity index 84%
rename from stdlib/robustness.mlw
rename to stdlib/robust.mlw
index 1142f8ce941b2712d2383e9c394f690636aad6a7..4c7853dd7aecfe7fd29a84372c7ddcf2782803ff 100644
--- a/stdlib/robustness.mlw
+++ b/stdlib/robust.mlw
@@ -43,22 +43,22 @@ theory RobustDatasetCSV
    predicate bounded_by_epsilon (e: elt) (eps: t) =
      forall v: index. valid_index e v -> .- eps .<= e[v] .<= eps
 
-   predicate robust_around (advises: elt -> label_ -> bool) (eps: t) (l: label_) (e: elt) =
+   predicate advises (valid_label: label_ -> bool)
+                     (nn: nn) (e: elt) (l: label_) =
+     valid_label l ->
+     forall j: int. valid_label j -> j <> l -> (nn @@ e)[l] .>= (nn @@ e)[j]
+
+   predicate robust_around (valid_label: label_ -> bool)
+                           (nn: nn) (eps: t) (l: label_) (e: elt) =
      forall perturbed_elt: elt.
        has_length perturbed_elt (length e) ->
        valid_elt perturbed_elt ->
        let perturbation = perturbed_elt - e in
        bounded_by_epsilon perturbation eps ->
-       advises perturbed_elt l
-
-  predicate advises (valid_label: label_ -> bool) (nn: nn) (e: elt) (l: label_) =
-     valid_label l ->
-     forall j: int. valid_label j -> j <> l -> (nn @@ e)[l] .>= (nn @@ e)[j]
+       advises valid_label nn perturbed_elt l
 
-   predicate robust (nn: nn) (d: dataset t) (eps: t) =
-     let min_label = DatasetCSV.min_label d in
-     let max_label = DatasetCSV.max_label d in
-     let advises = advises (valid_label min_label max_label) nn in
-     DatasetCSV.forall_ d (robust_around advises eps)
+   predicate robust (valid_label: label_ -> bool)
+                    (nn: nn) (d: dataset t) (eps: t) =
+     DatasetCSV.forall_ d (robust_around valid_label nn eps)
 
 end
\ No newline at end of file
diff --git a/tests/interpretation_acasxu.t b/tests/acasxu.t
similarity index 99%
rename from tests/interpretation_acasxu.t
rename to tests/acasxu.t
index a80981939c156d31af70d001e5be233631c16e76..7be456ba98bb2928b0cdfc9bb48ffaf545891440 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/acasxu.t
@@ -1,4 +1,4 @@
-Test interpret on acasxu
+Test verify on acasxu
   $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
diff --git a/tests/dataset.t b/tests/dataset.t
index 3476ac347cb8be7906ce2fa4b828d711cbb16287..af53aeed3a81a64a0f36d3368c02813805a07d4a 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -1,5 +1,5 @@
 Test verify on dataset
-  $ cat - > test_data.csv << EOF
+  $ cat - > dataset.csv << EOF
   > 1,0.0,1.0,0.784313725,0.019607843,0.776470588
   > 0,0.941176471,0,0,0.011764706,0.039215686
   > EOF
@@ -12,19 +12,29 @@ Test verify on dataset
   $ bin/Marabou --version
   1.0.+
 
-  $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ cat > file.mlw << EOF
   > theory T
-  >   use TestNetwork.AsArray as TN
   >   use ieee_float.Float64
-  >   use caisar.DatasetClassification
-  >   use caisar.DatasetClassificationProps
+  >   use int.Int
+  >   use nn.NeuralNetwork
+  >   use dataset.DatasetCSV
+  >   use robust.RobustDatasetCSV
   > 
-  >   goal G: correct TN.model dataset
+  >   constant min_label: label_ = 0
+  >   constant max_label: label_ = 4
+  > 
+  >   predicate valid_label (l: label_) =
+  >     RobustDatasetCSV.valid_label min_label max_label l
   > 
   >   goal H:
-  >    robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
+  >     let nn = read_neural_network "TestNetwork.nnet" NNet in
+  >     let dataset = read_dataset_csv "dataset.csv" in
+  >     let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
+  >     robust valid_label nn dataset eps
   > end
   > EOF
+
+  $ caisar verify --ltag=ProverSpec -p PyRAT --prover-altern=VNNLIB file.mlw 2>&1 | ./filter_tmpdir.sh
   [DEBUG]{ProverSpec} Prover-tailored specification:
   ;;; produced by PyRAT/VNN-LIB driver
   ;;; produced by VNN-LIB driver
@@ -43,6 +53,66 @@ Test verify on dataset
   ;; X_4
   (declare-const X_4 Real)
   
+  ;; H
+  (assert (>= X_0 0.0))
+  
+  ;; H
+  (assert (<= X_0 1.0))
+  
+  ;; H
+  (assert (>= X_1 0.0))
+  
+  ;; H
+  (assert (<= X_1 1.0))
+  
+  ;; H
+  (assert (>= X_2 0.0))
+  
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
+  
+  ;; H
+  (assert (<= X_3 1.0))
+  
+  ;; H
+  (assert (>= X_4 0.0))
+  
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
+  (assert (>= X_0 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_0 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_1 0.9899999999999999911182158029987476766109466552734375))
+  
+  ;; H
+  (assert (<= X_1 1.0100000000000000088817841970012523233890533447265625))
+  
+  ;; H
+  (assert (>= X_2 0.77431372499999995273611830270965583622455596923828125))
+  
+  ;; H
+  (assert (<= X_2 0.79431372499999997049968669671216048300266265869140625))
+  
+  ;; H
+  (assert (>= X_3 0.00960784299999999959196461674082456738688051700592041015625))
+  
+  ;; H
+  (assert (<= X_3 0.029607843000000001743021726952065364457666873931884765625))
+  
+  ;; H
+  (assert (>= X_4 0.7664705880000000082219457908649928867816925048828125))
+  
+  ;; H
+  (assert (<= X_4 0.7864705880000000259855141848674975335597991943359375))
+  
   ;; Y_0
   (declare-const Y_0 Real)
   
@@ -58,44 +128,104 @@ Test verify on dataset
   ;; Y_4
   (declare-const Y_4 Real)
   
-  ;; axiom_ge_x0
+  ;; Goal H
+  (assert (>= Y_0 Y_1))
+  
+  [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)
+  
+  ;; H
   (assert (>= X_0 0.0))
   
-  ;; axiom_le_x0
-  (assert (<= X_0 0.0))
+  ;; H
+  (assert (<= X_0 1.0))
   
-  ;; axiom_ge_x1
-  (assert (>= X_1 1.0))
+  ;; H
+  (assert (>= X_1 0.0))
   
-  ;; axiom_le_x1
+  ;; H
   (assert (<= X_1 1.0))
   
-  ;; axiom_ge_x2
-  (assert (>= X_2 0.78431372499999996161790249971090815961360931396484375))
+  ;; H
+  (assert (>= X_2 0.0))
+  
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
+  
+  ;; H
+  (assert (<= X_3 1.0))
+  
+  ;; H
+  (assert (>= X_4 0.0))
+  
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
+  (assert (>= X_0 -0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; axiom_le_x2
-  (assert (<= X_2 0.78431372499999996161790249971090815961360931396484375))
+  ;; H
+  (assert (<= X_0 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_1 0.9899999999999999911182158029987476766109466552734375))
+  
+  ;; H
+  (assert (<= X_1 1.0100000000000000088817841970012523233890533447265625))
   
-  ;; axiom_ge_x3
-  (assert (>= X_3 0.01960784299999999980013143385804141871631145477294921875))
+  ;; H
+  (assert (>= X_2 0.77431372499999995273611830270965583622455596923828125))
+  
+  ;; H
+  (assert (<= X_2 0.79431372499999997049968669671216048300266265869140625))
+  
+  ;; H
+  (assert (>= X_3 0.00960784299999999959196461674082456738688051700592041015625))
+  
+  ;; H
+  (assert (<= X_3 0.029607843000000001743021726952065364457666873931884765625))
+  
+  ;; H
+  (assert (>= X_4 0.7664705880000000082219457908649928867816925048828125))
+  
+  ;; H
+  (assert (<= X_4 0.7864705880000000259855141848674975335597991943359375))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
   
-  ;; axiom_le_x3
-  (assert (<= X_3 0.01960784299999999980013143385804141871631145477294921875))
+  ;; Y_2
+  (declare-const Y_2 Real)
   
-  ;; axiom_ge_x4
-  (assert (>= X_4 0.776470588000000017103729987866245210170745849609375))
+  ;; Y_3
+  (declare-const Y_3 Real)
   
-  ;; axiom_le_x4
-  (assert (<= X_4 0.776470588000000017103729987866245210170745849609375))
+  ;; Y_4
+  (declare-const Y_4 Real)
   
-  ;; Goal correct_record0_y1
-  (assert
-    (or
-      (and (>= Y_0 Y_1))
-      (and (>= Y_2 Y_1))
-      (and (>= Y_3 Y_1))
-      (and (>= Y_4 Y_1))
-      ))
+  ;; Goal H
+  (assert (>= Y_2 Y_1))
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   ;;; produced by PyRAT/VNN-LIB driver
@@ -115,6 +245,66 @@ Test verify on dataset
   ;; X_4
   (declare-const X_4 Real)
   
+  ;; H
+  (assert (>= X_0 0.0))
+  
+  ;; H
+  (assert (<= X_0 1.0))
+  
+  ;; H
+  (assert (>= X_1 0.0))
+  
+  ;; H
+  (assert (<= X_1 1.0))
+  
+  ;; H
+  (assert (>= X_2 0.0))
+  
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
+  
+  ;; H
+  (assert (<= X_3 1.0))
+  
+  ;; H
+  (assert (>= X_4 0.0))
+  
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
+  (assert (>= X_0 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_0 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_1 0.9899999999999999911182158029987476766109466552734375))
+  
+  ;; H
+  (assert (<= X_1 1.0100000000000000088817841970012523233890533447265625))
+  
+  ;; H
+  (assert (>= X_2 0.77431372499999995273611830270965583622455596923828125))
+  
+  ;; H
+  (assert (<= X_2 0.79431372499999997049968669671216048300266265869140625))
+  
+  ;; H
+  (assert (>= X_3 0.00960784299999999959196461674082456738688051700592041015625))
+  
+  ;; H
+  (assert (<= X_3 0.029607843000000001743021726952065364457666873931884765625))
+  
+  ;; H
+  (assert (>= X_4 0.7664705880000000082219457908649928867816925048828125))
+  
+  ;; H
+  (assert (<= X_4 0.7864705880000000259855141848674975335597991943359375))
+  
   ;; Y_0
   (declare-const Y_0 Real)
   
@@ -130,44 +320,104 @@ Test verify on dataset
   ;; Y_4
   (declare-const Y_4 Real)
   
-  ;; axiom_ge_x0
-  (assert (>= X_0 0.94117647100000001447739350624033249914646148681640625))
+  ;; Goal H
+  (assert (>= Y_3 Y_1))
+  
+  [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)
   
-  ;; axiom_le_x0
-  (assert (<= X_0 0.94117647100000001447739350624033249914646148681640625))
+  ;; H
+  (assert (>= X_0 0.0))
   
-  ;; axiom_ge_x1
+  ;; H
+  (assert (<= X_0 1.0))
+  
+  ;; H
   (assert (>= X_1 0.0))
   
-  ;; axiom_le_x1
-  (assert (<= X_1 0.0))
+  ;; H
+  (assert (<= X_1 1.0))
   
-  ;; axiom_ge_x2
+  ;; H
   (assert (>= X_2 0.0))
   
-  ;; axiom_le_x2
-  (assert (<= X_2 0.0))
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
   
-  ;; axiom_ge_x3
-  (assert (>= X_3 0.01176470599999999977480769075555144809186458587646484375))
+  ;; H
+  (assert (<= X_3 1.0))
   
-  ;; axiom_le_x3
-  (assert (<= X_3 0.01176470599999999977480769075555144809186458587646484375))
+  ;; H
+  (assert (>= X_4 0.0))
   
-  ;; axiom_ge_x4
-  (assert (>= X_4 0.0392156859999999996002628677160828374326229095458984375))
+  ;; H
+  (assert (<= X_4 1.0))
   
-  ;; axiom_le_x4
-  (assert (<= X_4 0.0392156859999999996002628677160828374326229095458984375))
+  ;; H
+  (assert (>= X_0 -0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; Goal correct_record1_y0
-  (assert
-    (or
-      (and (>= Y_1 Y_0))
-      (and (>= Y_2 Y_0))
-      (and (>= Y_3 Y_0))
-      (and (>= Y_4 Y_0))
-      ))
+  ;; H
+  (assert (<= X_0 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_1 0.9899999999999999911182158029987476766109466552734375))
+  
+  ;; H
+  (assert (<= X_1 1.0100000000000000088817841970012523233890533447265625))
+  
+  ;; H
+  (assert (>= X_2 0.77431372499999995273611830270965583622455596923828125))
+  
+  ;; H
+  (assert (<= X_2 0.79431372499999997049968669671216048300266265869140625))
+  
+  ;; H
+  (assert (>= X_3 0.00960784299999999959196461674082456738688051700592041015625))
+  
+  ;; H
+  (assert (<= X_3 0.029607843000000001743021726952065364457666873931884765625))
+  
+  ;; H
+  (assert (>= X_4 0.7664705880000000082219457908649928867816925048828125))
+  
+  ;; H
+  (assert (<= X_4 0.7864705880000000259855141848674975335597991943359375))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; Goal H
+  (assert (>= Y_4 Y_1))
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   ;;; produced by PyRAT/VNN-LIB driver
@@ -187,6 +437,66 @@ Test verify on dataset
   ;; X_4
   (declare-const X_4 Real)
   
+  ;; H
+  (assert (>= X_0 0.0))
+  
+  ;; H
+  (assert (<= X_0 1.0))
+  
+  ;; H
+  (assert (>= X_1 0.0))
+  
+  ;; H
+  (assert (<= X_1 1.0))
+  
+  ;; H
+  (assert (>= X_2 0.0))
+  
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
+  
+  ;; H
+  (assert (<= X_3 1.0))
+  
+  ;; H
+  (assert (>= X_4 0.0))
+  
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
+  (assert (>= X_0 0.93117647100000000559560930923908017575740814208984375))
+  
+  ;; H
+  (assert (<= X_0 0.95117647100000002335917770324158482253551483154296875))
+  
+  ;; H
+  (assert (>= X_1 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_1 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_2 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_2 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_3 0.00176470599999999956664087363833459676243364810943603515625))
+  
+  ;; H
+  (assert (<= X_3 0.021764706000000001717697983849575393833220005035400390625))
+  
+  ;; H
+  (assert (>= X_4 0.029215685999999997657372574622058891691267490386962890625))
+  
+  ;; H
+  (assert (<= X_4 0.049215686000000001543153160810106783173978328704833984375))
+  
   ;; Y_0
   (declare-const Y_0 Real)
   
@@ -202,44 +512,104 @@ Test verify on dataset
   ;; Y_4
   (declare-const Y_4 Real)
   
-  ;; axiom_ge_x0
+  ;; Goal H
+  (assert (>= Y_1 Y_0))
+  
+  [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)
+  
+  ;; H
   (assert (>= X_0 0.0))
   
-  ;; axiom_le_x0
-  (assert (<= X_0 0.01000000000000000020816681711721685132943093776702880859375))
+  ;; H
+  (assert (<= X_0 1.0))
   
-  ;; axiom_ge_x1
-  (assert (>= X_1 0.9899999999999999911182158029987476766109466552734375))
+  ;; H
+  (assert (>= X_1 0.0))
   
-  ;; axiom_le_x1
+  ;; H
   (assert (<= X_1 1.0))
   
-  ;; axiom_ge_x2
-  (assert (>= X_2 0.77431372499999995273611830270965583622455596923828125))
+  ;; H
+  (assert (>= X_2 0.0))
   
-  ;; axiom_le_x2
-  (assert (<= X_2 0.79431372499999997049968669671216048300266265869140625))
+  ;; H
+  (assert (<= X_2 1.0))
   
-  ;; axiom_ge_x3
-  (assert (>= X_3 0.00960784299999999959196461674082456738688051700592041015625))
+  ;; H
+  (assert (>= X_3 0.0))
   
-  ;; axiom_le_x3
-  (assert (<= X_3 0.029607843000000001743021726952065364457666873931884765625))
+  ;; H
+  (assert (<= X_3 1.0))
   
-  ;; axiom_ge_x4
-  (assert (>= X_4 0.7664705880000000082219457908649928867816925048828125))
+  ;; H
+  (assert (>= X_4 0.0))
   
-  ;; axiom_le_x4
-  (assert (<= X_4 0.7864705880000000259855141848674975335597991943359375))
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
+  (assert (>= X_0 0.93117647100000000559560930923908017575740814208984375))
+  
+  ;; H
+  (assert (<= X_0 0.95117647100000002335917770324158482253551483154296875))
+  
+  ;; H
+  (assert (>= X_1 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_1 0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; Goal robust_record0_y1
-  (assert
-    (or
-      (and (>= Y_0 Y_1))
-      (and (>= Y_2 Y_1))
-      (and (>= Y_3 Y_1))
-      (and (>= Y_4 Y_1))
-      ))
+  ;; H
+  (assert (>= X_2 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_2 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_3 0.00176470599999999956664087363833459676243364810943603515625))
+  
+  ;; H
+  (assert (<= X_3 0.021764706000000001717697983849575393833220005035400390625))
+  
+  ;; H
+  (assert (>= X_4 0.029215685999999997657372574622058891691267490386962890625))
+  
+  ;; H
+  (assert (<= X_4 0.049215686000000001543153160810106783173978328704833984375))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; Goal H
+  (assert (>= Y_2 Y_0))
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   ;;; produced by PyRAT/VNN-LIB driver
@@ -259,6 +629,66 @@ Test verify on dataset
   ;; X_4
   (declare-const X_4 Real)
   
+  ;; H
+  (assert (>= X_0 0.0))
+  
+  ;; H
+  (assert (<= X_0 1.0))
+  
+  ;; H
+  (assert (>= X_1 0.0))
+  
+  ;; H
+  (assert (<= X_1 1.0))
+  
+  ;; H
+  (assert (>= X_2 0.0))
+  
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
+  
+  ;; H
+  (assert (<= X_3 1.0))
+  
+  ;; H
+  (assert (>= X_4 0.0))
+  
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
+  (assert (>= X_0 0.93117647100000000559560930923908017575740814208984375))
+  
+  ;; H
+  (assert (<= X_0 0.95117647100000002335917770324158482253551483154296875))
+  
+  ;; H
+  (assert (>= X_1 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_1 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_2 -0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (<= X_2 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; H
+  (assert (>= X_3 0.00176470599999999956664087363833459676243364810943603515625))
+  
+  ;; H
+  (assert (<= X_3 0.021764706000000001717697983849575393833220005035400390625))
+  
+  ;; H
+  (assert (>= X_4 0.029215685999999997657372574622058891691267490386962890625))
+  
+  ;; H
+  (assert (<= X_4 0.049215686000000001543153160810106783173978328704833984375))
+  
   ;; Y_0
   (declare-const Y_0 Real)
   
@@ -274,170 +704,123 @@ Test verify on dataset
   ;; Y_4
   (declare-const Y_4 Real)
   
-  ;; axiom_ge_x0
+  ;; Goal H
+  (assert (>= Y_3 Y_0))
+  
+  [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)
+  
+  ;; H
+  (assert (>= X_0 0.0))
+  
+  ;; H
+  (assert (<= X_0 1.0))
+  
+  ;; H
+  (assert (>= X_1 0.0))
+  
+  ;; H
+  (assert (<= X_1 1.0))
+  
+  ;; H
+  (assert (>= X_2 0.0))
+  
+  ;; H
+  (assert (<= X_2 1.0))
+  
+  ;; H
+  (assert (>= X_3 0.0))
+  
+  ;; H
+  (assert (<= X_3 1.0))
+  
+  ;; H
+  (assert (>= X_4 0.0))
+  
+  ;; H
+  (assert (<= X_4 1.0))
+  
+  ;; H
   (assert (>= X_0 0.93117647100000000559560930923908017575740814208984375))
   
-  ;; axiom_le_x0
+  ;; H
   (assert (<= X_0 0.95117647100000002335917770324158482253551483154296875))
   
-  ;; axiom_ge_x1
-  (assert (>= X_1 0.0))
+  ;; H
+  (assert (>= X_1 -0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; axiom_le_x1
+  ;; H
   (assert (<= X_1 0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; axiom_ge_x2
-  (assert (>= X_2 0.0))
+  ;; H
+  (assert (>= X_2 -0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; axiom_le_x2
+  ;; H
   (assert (<= X_2 0.01000000000000000020816681711721685132943093776702880859375))
   
-  ;; axiom_ge_x3
+  ;; H
   (assert (>= X_3 0.00176470599999999956664087363833459676243364810943603515625))
   
-  ;; axiom_le_x3
+  ;; H
   (assert (<= X_3 0.021764706000000001717697983849575393833220005035400390625))
   
-  ;; axiom_ge_x4
+  ;; H
   (assert (>= X_4 0.029215685999999997657372574622058891691267490386962890625))
   
-  ;; axiom_le_x4
+  ;; H
   (assert (<= X_4 0.049215686000000001543153160810106783173978328704833984375))
   
-  ;; Goal robust_record1_y0
-  (assert
-    (or
-      (and (>= Y_1 Y_0))
-      (and (>= Y_2 Y_0))
-      (and (>= Y_3 Y_0))
-      (and (>= Y_4 Y_0))
-      ))
-  
-  Goal G: Unknown ()
-  Goal H: Unknown ()
-
-  $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
-  > theory T
-  >   use TestNetwork.AsArray as TN
-  >   use ieee_float.Float64
-  >   use caisar.DatasetClassification
-  >   use caisar.DatasetClassificationProps
-  > 
-  >   goal G: correct TN.model dataset
-  > 
-  >   goal H:
-  >    robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
-  > end
-  > EOF
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 0.0
-  x1 >= 1.0
-  x1 <= 1.0
-  x2 >= 0.78431372499999996161790249971090815961360931396484375
-  x2 <= 0.78431372499999996161790249971090815961360931396484375
-  x3 >= 0.01960784299999999980013143385804141871631145477294921875
-  x3 <= 0.01960784299999999980013143385804141871631145477294921875
-  x4 >= 0.776470588000000017103729987866245210170745849609375
-  x4 <= 0.776470588000000017103729987866245210170745849609375
-  +y0 -y1 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 0.0
-  x1 >= 1.0
-  x1 <= 1.0
-  x2 >= 0.78431372499999996161790249971090815961360931396484375
-  x2 <= 0.78431372499999996161790249971090815961360931396484375
-  x3 >= 0.01960784299999999980013143385804141871631145477294921875
-  x3 <= 0.01960784299999999980013143385804141871631145477294921875
-  x4 >= 0.776470588000000017103729987866245210170745849609375
-  x4 <= 0.776470588000000017103729987866245210170745849609375
-  +y2 -y1 >= 0
+  ;; Y_0
+  (declare-const Y_0 Real)
   
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 0.0
-  x1 >= 1.0
-  x1 <= 1.0
-  x2 >= 0.78431372499999996161790249971090815961360931396484375
-  x2 <= 0.78431372499999996161790249971090815961360931396484375
-  x3 >= 0.01960784299999999980013143385804141871631145477294921875
-  x3 <= 0.01960784299999999980013143385804141871631145477294921875
-  x4 >= 0.776470588000000017103729987866245210170745849609375
-  x4 <= 0.776470588000000017103729987866245210170745849609375
-  +y3 -y1 >= 0
+  ;; Y_1
+  (declare-const Y_1 Real)
   
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 0.0
-  x1 >= 1.0
-  x1 <= 1.0
-  x2 >= 0.78431372499999996161790249971090815961360931396484375
-  x2 <= 0.78431372499999996161790249971090815961360931396484375
-  x3 >= 0.01960784299999999980013143385804141871631145477294921875
-  x3 <= 0.01960784299999999980013143385804141871631145477294921875
-  x4 >= 0.776470588000000017103729987866245210170745849609375
-  x4 <= 0.776470588000000017103729987866245210170745849609375
-  +y4 -y1 >= 0
+  ;; Y_2
+  (declare-const Y_2 Real)
   
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.94117647100000001447739350624033249914646148681640625
-  x0 <= 0.94117647100000001447739350624033249914646148681640625
-  x1 >= 0.0
-  x1 <= 0.0
-  x2 >= 0.0
-  x2 <= 0.0
-  x3 >= 0.01176470599999999977480769075555144809186458587646484375
-  x3 <= 0.01176470599999999977480769075555144809186458587646484375
-  x4 >= 0.0392156859999999996002628677160828374326229095458984375
-  x4 <= 0.0392156859999999996002628677160828374326229095458984375
-  +y1 -y0 >= 0
+  ;; Y_3
+  (declare-const Y_3 Real)
   
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.94117647100000001447739350624033249914646148681640625
-  x0 <= 0.94117647100000001447739350624033249914646148681640625
-  x1 >= 0.0
-  x1 <= 0.0
-  x2 >= 0.0
-  x2 <= 0.0
-  x3 >= 0.01176470599999999977480769075555144809186458587646484375
-  x3 <= 0.01176470599999999977480769075555144809186458587646484375
-  x4 >= 0.0392156859999999996002628677160828374326229095458984375
-  x4 <= 0.0392156859999999996002628677160828374326229095458984375
-  +y2 -y0 >= 0
+  ;; Y_4
+  (declare-const Y_4 Real)
   
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.94117647100000001447739350624033249914646148681640625
-  x0 <= 0.94117647100000001447739350624033249914646148681640625
-  x1 >= 0.0
-  x1 <= 0.0
-  x2 >= 0.0
-  x2 <= 0.0
-  x3 >= 0.01176470599999999977480769075555144809186458587646484375
-  x3 <= 0.01176470599999999977480769075555144809186458587646484375
-  x4 >= 0.0392156859999999996002628677160828374326229095458984375
-  x4 <= 0.0392156859999999996002628677160828374326229095458984375
-  +y3 -y0 >= 0
+  ;; Goal H
+  (assert (>= Y_4 Y_0))
   
+  Goal H: Unknown ()
+
+  $ caisar verify --ltag=ProverSpec -p Marabou file.mlw 2>&1 | ./filter_tmpdir.sh
   [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.94117647100000001447739350624033249914646148681640625
-  x0 <= 0.94117647100000001447739350624033249914646148681640625
+  x0 >= 0.0
+  x0 <= 1.0
   x1 >= 0.0
-  x1 <= 0.0
+  x1 <= 1.0
   x2 >= 0.0
-  x2 <= 0.0
-  x3 >= 0.01176470599999999977480769075555144809186458587646484375
-  x3 <= 0.01176470599999999977480769075555144809186458587646484375
-  x4 >= 0.0392156859999999996002628677160828374326229095458984375
-  x4 <= 0.0392156859999999996002628677160828374326229095458984375
-  +y4 -y0 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
   x0 <= 0.01000000000000000020816681711721685132943093776702880859375
   x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0
+  x1 <= 1.0100000000000000088817841970012523233890533447265625
   x2 >= 0.77431372499999995273611830270965583622455596923828125
   x2 <= 0.79431372499999997049968669671216048300266265869140625
   x3 >= 0.00960784299999999959196461674082456738688051700592041015625
@@ -448,9 +831,19 @@ Test verify on dataset
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
   x0 <= 0.01000000000000000020816681711721685132943093776702880859375
   x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0
+  x1 <= 1.0100000000000000088817841970012523233890533447265625
   x2 >= 0.77431372499999995273611830270965583622455596923828125
   x2 <= 0.79431372499999997049968669671216048300266265869140625
   x3 >= 0.00960784299999999959196461674082456738688051700592041015625
@@ -461,9 +854,19 @@ Test verify on dataset
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
   x0 <= 0.01000000000000000020816681711721685132943093776702880859375
   x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0
+  x1 <= 1.0100000000000000088817841970012523233890533447265625
   x2 >= 0.77431372499999995273611830270965583622455596923828125
   x2 <= 0.79431372499999997049968669671216048300266265869140625
   x3 >= 0.00960784299999999959196461674082456738688051700592041015625
@@ -474,9 +877,19 @@ Test verify on dataset
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
   x0 <= 0.01000000000000000020816681711721685132943093776702880859375
   x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0
+  x1 <= 1.0100000000000000088817841970012523233890533447265625
   x2 >= 0.77431372499999995273611830270965583622455596923828125
   x2 <= 0.79431372499999997049968669671216048300266265869140625
   x3 >= 0.00960784299999999959196461674082456738688051700592041015625
@@ -486,11 +899,21 @@ Test verify on dataset
   +y4 -y1 >= 0
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
   x0 >= 0.93117647100000000559560930923908017575740814208984375
   x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= 0.0
+  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
   x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= 0.0
+  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
   x2 <= 0.01000000000000000020816681711721685132943093776702880859375
   x3 >= 0.00176470599999999956664087363833459676243364810943603515625
   x3 <= 0.021764706000000001717697983849575393833220005035400390625
@@ -499,11 +922,21 @@ Test verify on dataset
   +y1 -y0 >= 0
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
   x0 >= 0.93117647100000000559560930923908017575740814208984375
   x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= 0.0
+  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
   x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= 0.0
+  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
   x2 <= 0.01000000000000000020816681711721685132943093776702880859375
   x3 >= 0.00176470599999999956664087363833459676243364810943603515625
   x3 <= 0.021764706000000001717697983849575393833220005035400390625
@@ -512,11 +945,21 @@ Test verify on dataset
   +y2 -y0 >= 0
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
   x0 >= 0.93117647100000000559560930923908017575740814208984375
   x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= 0.0
+  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
   x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= 0.0
+  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
   x2 <= 0.01000000000000000020816681711721685132943093776702880859375
   x3 >= 0.00176470599999999956664087363833459676243364810943603515625
   x3 <= 0.021764706000000001717697983849575393833220005035400390625
@@ -525,11 +968,21 @@ Test verify on dataset
   +y3 -y0 >= 0
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
   x0 >= 0.93117647100000000559560930923908017575740814208984375
   x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= 0.0
+  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
   x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= 0.0
+  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
   x2 <= 0.01000000000000000020816681711721685132943093776702880859375
   x3 >= 0.00176470599999999956664087363833459676243364810943603515625
   x3 <= 0.021764706000000001717697983849575393833220005035400390625
@@ -537,5 +990,4 @@ Test verify on dataset
   x4 <= 0.049215686000000001543153160810106783173978328704833984375
   +y4 -y0 >= 0
   
-  Goal G: Unknown ()
   Goal H: Unknown ()
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
deleted file mode 100644
index d4e8cbd413e2aa98073207d9cfe92b804e7c4aa4..0000000000000000000000000000000000000000
--- a/tests/interpretation_dataset.t
+++ /dev/null
@@ -1,119 +0,0 @@
-Test interpret on dataset
-  $ cat - > dataset.csv << EOF
-  > 2,0.0,1.0,0.784313725,0.019607843,0.776470588
-  > 0,0.941176471,0,0,0.011764706,0.039215686
-  > EOF
-
-  $ . ./setup_env.sh
-
-  $ bin/Marabou --version
-  1.0.+
-
-  $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh
-  > theory T
-  >   use ieee_float.Float64
-  >   use int.Int
-  >   use nn.NeuralNetwork
-  >   use dataset.DatasetCSV
-  >   use robustness.RobustDatasetCSV
-  > 
-  >   goal G:
-  >     let nn = read_neural_network "TestNetwork.nnet" NNet in
-  >     let dataset = read_dataset_csv "dataset.csv" in
-  >     let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
-  >     robust nn dataset eps
-  > end
-  > EOF
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0100000000000000088817841970012523233890533447265625
-  x2 >= 0.77431372499999995273611830270965583622455596923828125
-  x2 <= 0.79431372499999997049968669671216048300266265869140625
-  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
-  x3 <= 0.029607843000000001743021726952065364457666873931884765625
-  x4 >= 0.7664705880000000082219457908649928867816925048828125
-  x4 <= 0.7864705880000000259855141848674975335597991943359375
-  +y0 -y2 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0100000000000000088817841970012523233890533447265625
-  x2 >= 0.77431372499999995273611830270965583622455596923828125
-  x2 <= 0.79431372499999997049968669671216048300266265869140625
-  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
-  x3 <= 0.029607843000000001743021726952065364457666873931884765625
-  x4 >= 0.7664705880000000082219457908649928867816925048828125
-  x4 <= 0.7864705880000000259855141848674975335597991943359375
-  +y1 -y2 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= 0.93117647100000000559560930923908017575740814208984375
-  x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
-  x3 <= 0.021764706000000001717697983849575393833220005035400390625
-  x4 >= 0.029215685999999997657372574622058891691267490386962890625
-  x4 <= 0.049215686000000001543153160810106783173978328704833984375
-  +y1 -y0 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= 0.93117647100000000559560930923908017575740814208984375
-  x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
-  x3 <= 0.021764706000000001717697983849575393833220005035400390625
-  x4 >= 0.029215685999999997657372574622058891691267490386962890625
-  x4 <= 0.049215686000000001543153160810106783173978328704833984375
-  +y2 -y0 >= 0
-  
-  Goal G: Unknown ()