Check_IsIdempotent has a bug

[yamaguchi1024]

This bug can be reproduced by running apps/gemmini/src/exo/conv.py while putting unsafe_disable_check=False to add_loop(...). The code below is from the first add_loop in schedule_conv_17().

        for krow in seq(0, 3):
            for kcol in seq(0, 3):
                for orow_i in seq(0, 14):
                    if orow_i == 0:
                        for kch_o in seq(0, 8):
                            for och_o_o in seq(0, 2):
                                do_ld_i8_block_id1(
                                    16, 4,
                                    weights[krow, kcol,
                                            16 * kch_o:16 + 16 * kch_o,
                                            64 * och_o_o:64 + 64 * och_o_o],
                                    w_s[krow, kcol, kch_o,
                                        4 * och_o_o:4 + 4 * och_o_o, 0:16,
                                        0:16])

----> add_loop( conv, "if orow_i == 0:_", "orow_o", 2, guard=True) --->
should be able to produce

        for krow in seq(0, 3):
            for kcol in seq(0, 3):
                for orow_i in seq(0, 14):
                    for orow_o in seq(0, 2):
                        if orow_o == 0:
                            if orow_i == 0:
                                for kch_o in seq(0, 8):
                                    for och_o_o in seq(0, 2):
                                        do_ld_i8_block_id1(
                                            16, 4,
                                            weights[krow, kcol,
                                                    16 * kch_o:16 + 16 * kch_o,
                                                    64 * och_o_o:64 +
                                                    64 * och_o_o],
                                            w_s[krow, kcol, kch_o,
                                                4 * och_o_o:4 + 4 * och_o_o,
                                                0:16, 0:16])

but z3 gives an error instead.

Traceback (most recent call last):
  File "/opt/homebrew/bin/exocc", line 8, in <module>
    sys.exit(main())
             ^^^^^^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/main.py", line 40, in main
    library = [
              ^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/main.py", line 43, in <listcomp>
    for proc in get_procs_from_module(load_user_code(mod))
                                      ^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/main.py", line 92, in load_user_code
    loader.exec_module(user_module)
  File "<frozen importlib._bootstrap_external>", line 940, in exec_module
  File "<frozen importlib._bootstrap>", line 241, in _call_with_frames_removed
  File "/Users/yuka/exo/apps/gemmini/src/exo/conv.py", line 533, in <module>
    conv_17, conv_17_cpu = schedule_conv_17()
                           ^^^^^^^^^^^^^^^^^^
  File "/Users/yuka/exo/apps/gemmini/src/exo/conv.py", line 351, in schedule_conv_17
    conv = add_loop(
           ^^^^^^^^^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/API_scheduling.py", line 100, in __call__
    return self.func(*bound_args.args, **bound_args.kwargs)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/API_scheduling.py", line 2078, in add_loop
    ir, fwd = scheduling.DoAddLoop(
              ^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/LoopIR_scheduling.py", line 2567, in DoAddLoop
    Check_IsIdempotent(proc, [s])
  File "/opt/homebrew/lib/python3.11/site-packages/exo/new_eff.py", line 2091, in Check_IsIdempotent
    is_idempotent = slv.verify(ADef(Shadows(a, a)))
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/lib/python3.11/site-packages/exo/new_analysis_core.py", line 780, in verify
    raise TypeError("unknown result from z3")
TypeError: unknown result from z3