diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 00:35:33 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 00:35:33 -0300 |
| commit | 7aacf596d73cc74eb9af381a72723b50b4069e30 (patch) | |
| tree | 6970478e0866167285dc15820812b464407b75cb /test/test_embedding.ml | |
| parent | 6520b876af064d57bccf944a6fef9807a8c79de5 (diff) | |
| download | SOL-7aacf596d73cc74eb9af381a72723b50b4069e30.tar.gz SOL-7aacf596d73cc74eb9af381a72723b50b4069e30.zip | |
symbolic discharge: universals over infinite domains decided by intervals
Diffstat (limited to '')
| -rw-r--r-- | test/test_embedding.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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" |