From bb8288a0b46f345f3ba41032faf449b1e167d11e Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 17 Oct 2023 10:51:46 +0200 Subject: [PATCH] Adding missing tests --- tests/float/test_float3.ae | 5 +++++ tests/float/test_float3.expected | 2 ++ 2 files changed, 7 insertions(+) create mode 100644 tests/float/test_float3.ae create mode 100644 tests/float/test_float3.expected diff --git a/tests/float/test_float3.ae b/tests/float/test_float3.ae new file mode 100644 index 0000000000..3067a37b52 --- /dev/null +++ b/tests/float/test_float3.ae @@ -0,0 +1,5 @@ +logic x : real + +axiom ax : 1.0 <= x + +goal g : float(4, 4, NearestTiesToEven, 1.0) <= float(4, 4, NearestTiesToEven, x) \ No newline at end of file diff --git a/tests/float/test_float3.expected b/tests/float/test_float3.expected new file mode 100644 index 0000000000..6f99ff0f44 --- /dev/null +++ b/tests/float/test_float3.expected @@ -0,0 +1,2 @@ + +unsat