let
assume_node n ap = assume_node_no_check n ap;
SMT
.check ()