let assume_goal_no_check { tag = id; cube = cube } = 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