diff --git a/tests/pyrat.t b/tests/pyrat.t index 8de49dee6c3557d44a02175d5b021d33ce5ad9e1..da619dd4df7a1ce0b7e049117ddda5675d2c3020 100644 --- a/tests/pyrat.t +++ b/tests/pyrat.t @@ -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 () diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t index 8b65e0283171f9bd79860667d9a77169ca77ac52..d02b66118f3bb2d54be4187a894e0b52c0afa4e9 100644 --- a/tests/pyrat_onnx.t +++ b/tests/pyrat_onnx.t @@ -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 ()