Cubicle 1.1.2 documentation and source : Prover.reached

let reached args s sa =
  SMT.clear ();
  SMT.assume ~id:0 (distinct_vars (List.length args));
  let f = make_formula_set (SAtom.union sa s) in
  SMT.assume ~id:0 f;
  SMT.check ()