Cubicle 1.1.2 documentation and source : Prover.assume

let assume_goal n =
  assume_goal_no_check n;
  SMT.check  ()