Effect / Set failures, incomplete quantifiers

[jacobpake]

There are 3 tests recently failing in effects related files.

@buggymcbugfix perhaps related to #300 ?

https://github.com/granule-project/granule/blob/main/examples/effects_nondet.gr

    examples/effects_nondet.gr:                                                                   FAIL
      Exception: Type checking failed:
      Solver error: examples/effects_nondet.gr:21:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(prom_[21:50]0 = 2) ∧ (prom_[21:50]0..prom_[21:50]0 ≤ 0..∞) ∧ (2 = prom_[21:50]0)
      Solver error: examples/effects_nondet.gr:22:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(prom_[22:46]0 = 0) ∧ (prom_[22:46]0..prom_[22:46]0 ≤ 0..∞) ∧ (0 = prom_[22:46]0)
      Type error: examples/effects_nondet.gr:36:12:
      Expected `{?}` but got `e0`
      Type error: examples/effects_nondet.gr:44:24:
      Expected `{?}` but got `e1`
      Solver error: examples/effects_nondet.gr:51:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(e ⊆ e0) ∧ (0..∞ ≤ prom_[51:38]0) ∧ (0..∞ ≤ prom_[51:13]0)
      CallStack (from HasCallStack):
        error, called at interpreter/tests/Golden.hs:120:21 in main:Main
      Use -p '/examples\/effects_nondet.gr/' to rerun this test only.

https://github.com/granule-project/granule/blob/main/examples/effects_state.gr

    examples/effects_state.gr:                                                                    FAIL
      Exception: Type checking failed:
      Solver error: examples/effects_state.gr:21:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(prom_[21:45]0 = 1) ∧ (prom_[21:45]0..prom_[21:45]0 ≤ 0..∞) ∧ (1 = prom_[21:45]0)
      Solver error: examples/effects_state.gr:22:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(prom_[22:47]0 = 1) ∧ (prom_[22:43]0 ≤ 0..∞) ∧ (prom_[22:47]0..prom_[22:47]0 ≤ 0..∞) ∧ (1 = prom_[22:47]0) ∧ (0..∞ ≤ prom_[22:43]0)
      Solver error: examples/effects_state.gr:27:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	((1 : Nat) = 1) ∧ ((1 : Interval (Ext Nat)) + (0..∞) ≤ 0..∞)
      Type error: examples/effects_state.gr:33:8:
      Expected `{?}` but got `e0`
      Solver error: examples/effects_state.gr:43:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(e ⊆ e0) ∧ (0..∞ ≤ prom_[43:48]0) ∧ (0..∞ ≤ prom_[43:22]0)
      CallStack (from HasCallStack):
        error, called at interpreter/tests/Golden.hs:120:21 in main:Main
      Use -p '/examples\/effects_state.gr/' to rerun this test only.

https://github.com/granule-project/granule/blob/main/frontend/tests/cases/positive/effect-handlers/effects_state.gr

    frontend/tests/cases/positive/effect-handlers/effects_state.gr:                               FAIL
      Exception: Type checking failed:
      Solver error: frontend/tests/cases/positive/effect-handlers/effects_state.gr:21:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(prom_[21:45]0 = 1) ∧ (prom_[21:45]0..prom_[21:45]0 ≤ 0..∞) ∧ (1 = prom_[21:45]0)
      Solver error: frontend/tests/cases/positive/effect-handlers/effects_state.gr:22:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(prom_[22:47]0 = 1) ∧ (prom_[22:43]0 ≤ 0..∞) ∧ (prom_[22:47]0..prom_[22:47]0 ≤ 0..∞) ∧ (1 = prom_[22:47]0) ∧ (0..∞ ≤ prom_[22:43]0)
      Solver error: frontend/tests/cases/positive/effect-handlers/effects_state.gr:27:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	((1 : Nat) = 1) ∧ ((1 : Interval (Ext Nat)) + (0..∞) ≤ 0..∞)
      Type error: frontend/tests/cases/positive/effect-handlers/effects_state.gr:33:8:
      Expected `{?}` but got `e0`
      Solver error: frontend/tests/cases/positive/effect-handlers/effects_state.gr:43:1:
      smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
       for theorem:
      	(e ⊆ e0) ∧ (0..∞ ≤ prom_[43:48]0) ∧ (0..∞ ≤ prom_[43:22]0)
      CallStack (from HasCallStack):
        error, called at interpreter/tests/Golden.hs:120:21 in main:Main
      Use -p '/frontend\/tests\/cases\/positive\/effect-handlers\/effects_state.gr/' to rerun this test only.

[buggymcbugfix]

Tracked by #308