let sat p =
  match Prop.sat s.current p with
    | None -> 
        None
    | Some(rho, s') -> 
        let n = fresh_state_name () in
          s.symtab <- Symtab.add n (Symtab.State(s')) s.symtab;
          Some(rho, n)