diff options
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" |