[tests] Added test oracles to interpretation unit tests.

tests/interpretation_acasxu.t

@@ -7,7 +7,7 @@ Test interpret on acasxu
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ caisar verify -L . --format whyml --prover PyRAT --verbosity=info - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
   >   use bool.Bool
@@ -95,5 +95,42 @@ Test interpret on acasxu
   >       not (advises nn i clear_of_conflict)
   > end
   > EOF
+  [caisar][INFO] Specification to verify:
+  -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.60000151009774149724051994780893437564373016357421875 <= x0
+  0.450000000000000011102230246251565404236316680908203125 <= x3
+  x4 <= -0.450000000000000011102230246251565404236316680908203125
+  y0 <= 3.991125645861615112153231166303157806396484375
+  
+  [caisar][INFO] Specification to verify:
+  -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)
+  
+  [caisar][INFO] Verification results for theory 'T'
   [caisar] Goal P1: Unknown ()
   [caisar] Goal P3: Unknown ()

tests/interpretation_dataset.t

@@ -11,7 +11,7 @@ Test interpret on dataset
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ caisar verify -L . --format whyml --prover Marabou --verbosity=info - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
   >   use bool.Bool
@@ -53,4 +53,97 @@ Test interpret on dataset
   >     robust nn dataset eps
   > end
   > EOF
+  [caisar][INFO] Specification to verify:
+  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.375
+  x0 <= 0.375
+  x1 >= 0.625
+  x1 <= 1.375
+  x2 >= 0.40931372499999996161790249971090815961360931396484375
+  x2 <= 1.159313725000000072640204962226562201976776123046875
+  x3 >= -0.355392156999999986322080758327501825988292694091796875
+  x3 <= 0.394607843000000013677919241672498174011707305908203125
+  x4 >= 0.401470588000000017103729987866245210170745849609375
+  x4 <= 1.151470588000000017103729987866245210170745849609375
+  +y0 -y1 >= 0
+  
+  [caisar][INFO] Specification to verify:
+  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.375
+  x0 <= 0.375
+  x1 >= 0.625
+  x1 <= 1.375
+  x2 >= 0.40931372499999996161790249971090815961360931396484375
+  x2 <= 1.159313725000000072640204962226562201976776123046875
+  x3 >= -0.355392156999999986322080758327501825988292694091796875
+  x3 <= 0.394607843000000013677919241672498174011707305908203125
+  x4 >= 0.401470588000000017103729987866245210170745849609375
+  x4 <= 1.151470588000000017103729987866245210170745849609375
+  +y2 -y1 >= 0
+  
+  [caisar][INFO] Specification to verify:
+  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.625
+  x0 <= 1.375
+  x1 >= -0.375
+  x1 <= 0.375
+  x2 >= -0.355392156999999986322080758327501825988292694091796875
+  x2 <= 0.394607843000000013677919241672498174011707305908203125
+  x3 >= 0.401470588000000017103729987866245210170745849609375
+  x3 <= 1.151470588000000017103729987866245210170745849609375
+  x4 >= 0.40931372499999996161790249971090815961360931396484375
+  x4 <= 1.159313725000000072640204962226562201976776123046875
+  +y1 -y0 >= 0
+  
+  [caisar][INFO] Specification to verify:
+  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.625
+  x0 <= 1.375
+  x1 >= -0.375
+  x1 <= 0.375
+  x2 >= -0.355392156999999986322080758327501825988292694091796875
+  x2 <= 0.394607843000000013677919241672498174011707305908203125
+  x3 >= 0.401470588000000017103729987866245210170745849609375
+  x3 <= 1.151470588000000017103729987866245210170745849609375
+  x4 >= 0.40931372499999996161790249971090815961360931396484375
+  x4 <= 1.159313725000000072640204962226562201976776123046875
+  +y2 -y0 >= 0
+  
+  [caisar][INFO] Verification results for theory 'T'
   [caisar] Goal G: Unknown ()