It is also a good thing, because it helps to refine the theorem statement. At least, my humble experience in CS theory research is that I’d try to prove a theorem I want to be true, find a counterexample, refine the statement, and continue.

P.S. It helps that in CS lots of theorems are about either inductive or coinductive definitions.