Possible implies endpoint not giving correct result

[nwatson22]

I have a simple configuration with just a k cell and a Map.

  configuration <T color="yellow">
                  <k> $PGM:Pgm </k>
                  <state> .Map </state>
                </T>

And am passing in something that looks like this (before being converted to kore)

antecedent: <generatedTop>
  <T>
    <k>
      K_CELL
    </k>
    <state>
      STATE_CELL
    </state>
  </T>
  <generatedCounter>
    GENERATEDCOUNTER_CELL
  </generatedCounter>
</generatedTop>
consequent: #Exists X . #Exists Y . <generatedTop>
  <T>
    <k>
      K_CELL
    </k>
    <state>
      STATE_CELL
    </state>
  </T>
  <generatedCounter>
    GENERATEDCOUNTER_CELL
  </generatedCounter>
</generatedTop>
#And { true #Equals 0 >Int Y }
#And { true #Equals 0 <=Int X }

with the goal of figuring out if { true #Equals 0 >Int Y } #And { true #Equals 0 <=Int X } is satisfiable, and the endpoint returns satisfiable=false. In #3601 it is mentioned that this satisfiable field should actually be called "valid", but I thought this implication should actually be valid because { true #Equals 0 >Int Y } #And { true #Equals 0 <=Int X } is satisfiable and the variables X and Y are existentially quantified. It's possible I'm just not using the endpoint correctly or am not understanding something matching-logic related.

bug_report.tar.gz

[goodlyrottenapple]

I wonder if this is the culprit:

haskell-backend/kore/src/Kore/Reachability/Claim.hs

Lines 773 to 776 in 89b42dd

	rhsBottom <-
	fmap isBottom . liftSimplifier $
	SMT.Evaluator.filterMultiOr $srcLoc
	=<< Pattern.simplify right

we are calling simplify on the rhs without the existential quantifiers here

[goodlyrottenapple]

the above, together with #3193 are causing the issue