let rec is_sat (s, p) =
  try
    Is.initialize0 s p;
    eval_and_branch ();
    let (s', p') = Is.finalize () in
      Some(s', p')
  with 
      Jst.Inconsistent _ -> None

and eval_and_branch () =
  eval ()