Skip to content
Snippets Groups Projects
Commit d0375604 authored by Julien Girard-Satabin's avatar Julien Girard-Satabin Committed by Michele Alberti
Browse files

[tests] Promote tests following rebase

parent 32cdffef
No related branches found
No related tags found
No related merge requests found
......@@ -41,7 +41,7 @@ Test verify
> use int.Int
> use interpretation.Vector
> use interpretation.NeuralNetwork
>
>
> constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
> goal H:
......@@ -52,16 +52,46 @@ Test verify
> end
> EOF
[caisar][INFO] Task sent to prover:
0.0 < x0
x0 < 0.5
0.5 < x1
x1 < 1.0
(0.0 < y0 or 0.5 < y0) and 0.0 < y1 and y1 < 0.5
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
[caisar][INFO] Task sent to prover:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
0.0 < y1
[caisar][INFO] Task sent to prover:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
y1 < 0.5
[caisar][INFO] Task sent to prover:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
[caisar][INFO] Task sent to prover:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
0.0 < y1
[caisar][INFO] Task sent to prover:
0.375 < x0
x0 < 0.75
0.5 < x1
x1 < 1.0
(0.0 < y0 or 0.5 < y0) and 0.0 < y1 and y1 < 0.5
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
y1 < 0.5
[caisar][INFO] Verification results for theory 'PyRAT_oracle'
[caisar] Goal H: Unknown ()
......@@ -24,8 +24,14 @@ Test verify
> end
> EOF
[caisar][INFO] Task sent to prover:
0.0 < x0
x0 < 0.5
0.0 < y0 and y0 < 0.5
0.0 <= x0
x0 <= 0.5
0.0 < y0
[caisar][INFO] Task sent to prover:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
[caisar][INFO] Verification results for theory 'PyRAT_ONNX'
[caisar] Goal G: Unknown ()
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment