let check2 ctx expected_result =
  begin
    let (result,m) = Z3.check_and_get_model ctx in
    (match result with
    | Z3.L_FALSE ->
      printf "unsat\n";
    | Z3.L_UNDEF ->
      printf "unknown\n";
      printf "potential model:\n";
      display_model ctx stdout m;
    | Z3.L_TRUE ->
      printf "sat\n";
      display_model ctx stdout m;
    );
    if result != expected_result then exitf "unexpected result";
  end