let testModelCheck i =
  (* Add seed predicates, if any to system *)
  let seedPredsFile = Options.getValueOfString "pred" in
  let seedPreds = Predicate.conjoinL (Stats.time "read seeds" constructInitialPredicates seedPredsFile)
  in
  let initStateFile = Options.getValueOfString "init" in
  let initialState = Predicate.conjoinL (Stats.time "read initial state" constructInitialPredicates initStateFile) in
  TestModelChecker.test_model_check initialState seedPreds