src/HOL/Tools/refute.ML

         Output.priority "Invoking SAT solver...";
         (case SatSolver.invoke_solver satsolver fm of
           SatSolver.SATISFIABLE assignment =>
           (Output.priority ("*** Model found: ***\n" ^ print_model thy model
             (fn i => case assignment i of SOME b => b | NONE => true));
-           "genuine")
+           if maybe_spurious then "potential" else "genuine")
         | SatSolver.UNSATISFIABLE _ =>
           (Output.priority "No model exists.";
           case next_universe universe sizes minsize maxsize of
             SOME universe' => find_model_loop universe'
           | NONE           => (Output.priority