let
run () =
SMT
.check ()