From 7aacf596d73cc74eb9af381a72723b50b4069e30 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 00:35:33 -0300 Subject: symbolic discharge: universals over infinite domains decided by intervals --- test/test_embedding.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'test/test_embedding.ml') diff --git a/test/test_embedding.ml b/test/test_embedding.ml index ea55e4f..a2eab95 100644 --- a/test/test_embedding.ml +++ b/test/test_embedding.ml @@ -66,9 +66,12 @@ let test_kernel_scan () = | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error let test_kernel_totality () = + (* A universal over an infinite domain whose body the symbolic + fragment cannot read: neither enumerable nor provable, so it + must be rejected, embedding or not. *) match solve - {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} + {| [ForAll variable: X quantifier: [Integer value: X] body: [Sensor id: X]] |} with | Error (Sol.Vm.Non_total_plan _) -> () | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard" -- cgit v1.2.3