slim_check giving wrong counterexamples?

Stream: mathlib4

[Kim Morrison]

Maybe I am just dumb, but it appears that the counterexamples slim_check is producing here are all wrong:

import Mathlib

open Nat

theorem testBit_pred :
    testBit (pred x) i = (decide (0 < x) &&
      (Bool.xor ((List.range i).all fun j => ! testBit x j) (testBit x i))) := by
  slim_check -- proposes various small counterexamples of the form `x < 20`, `i = 1`.

-- None of which are actually counterexamples:
run_meta do
  for x in List.range 32 do
    for i in List.range 6 do
      if testBit (pred x) i != (decide (0 < x) &&
        (Bool.xor ((List.range i).all fun j => ! testBit x j) (testBit x i))) then
        IO.println (x, i)

Would anyone have time/inclination to look into this? slim_check is currently a rather incomplete implementation of a wonderful wonderful thing, and could use adoption or even just some attention.

[Eric Rodriguez]

I noticed it making some false counterexamples in something else recently, too

[Eric Wieser]

I have a PR open that probably fixes this

[Eric Wieser]

#9722

[Eric Wieser]

Unfortunately it's impossible to test because slim_check uses IO.println, but tests aren't allowed to write to stdout (see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/noisy.20tests/near/419142386)

[Mario Carneiro]

slim_check should be using logInfo instead of IO.println

[Eric Wieser]

Even though logInfo sometimes goes into the void?

[Mario Carneiro]

that's an issue with #eval (_ : MetaM _), not logInfo

[Eric Wieser]

Mario Carneiro said:

slim_check should be using logInfo instead of IO.println

Done in #10393

[Eric Wieser]

Eric Wieser said:

I have a PR open that probably fixes this

I added this as a test and can confirm the problem is gone after #9722