let assume_goal_nodes { tag = id; cube = cube } nodes = SMT.clear (); SMT.assume ~id (distinct_vars (List.length cube.Cube.vars)); let f = make_formula cube.Cube.array in if debug_smt then eprintf "[smt] goal g: %a@." F.print f; SMT.assume ~id f; List.iter (fun (n, a) -> assume_node_no_check n a) nodes; SMT.check ()