Can't simplify integer side-conditions

This input specification:

module TEST-SYNTAX 
    imports DOMAINS 
 
    syntax Pgm ::= "a" | "b" | "c" 
 
endmodule 

module TEST
    imports TEST-SYNTAX

    configuration <k> $PGM:Pgm </k> <i> 0 </i>

    rule <k> a => b ... </k> <i> I => I +Int 1 </i> requires I <=Int 10
    rule <k> b => a ... </k> <i> I => I +Int 1 </i> requires I <=Int 10
endmodule

and the proof (which is unprovable):

requires "test.k"

module TEST-SPEC
    imports TEST

    rule <k> a => c ... </k> <i> I => ?_ </i> requires I <=Int 0

endmodule

But proving it out to depth 4 causes this type of side-condition:

  #Not ( {
    I +Int 2 <=Int 0
  #Equals
    true
  } )
#And
  <generatedTop>
    <k>
      a ~> _DotVar1 ~> .
    </k>
    <i>
      I +Int 4
    </i>
  </generatedTop>
#And
  {
    I +Int 1 <=Int 10
  #Equals
    true
  }
#And
  {
    I +Int 2 <=Int 10
  #Equals
    true
  }
#And
  {
    I +Int 3 <=Int 10
  #Equals
    true
  }
#And
  {
    I <=Int 0
  #Equals
    true
  }
#And
  {
    I <=Int 10
  #Equals
    true
  }

Notice that we have I <=Int 0 and I +Int 3 <=Int 10, even though I <=Int 10 is trivially true given that I +Int 3 <=Int 10.

This may seem innocuous, but in KEVM it results in ever-growing side-conditions which look like this { 3 <=Int VGas +Int -3 #Equals true } #And { 3 <=Int VGas +Int -15 #Equals true }, and for a proof that runs for thousands of KEVM steps, this condition will grow quite large.

I added this rule to simplify it:

rule X <=Int Y +Int Z => X -Int Z <=Int Y [simplification, concrete(X, Z)]

which results in { 0 <=Int VGas #Equals true } #And { 18 <=Int VGas #Equals true }.

I tried adding these three rules independently, and neither seemed to work to remove the redundant side-conditions (also without the anywhere):

    rule X <=Int Y => true requires X <=Int Z andBool Z <=Int Y [simplification]
    rule X <=Int Y => true requires X <=Int ?Z andBool ?Z <=Int Y [simplification]
    rule { X <=Int Y #Equals true } #And { Z <=Int Y #Equals true } => { Z <=Int Y #Equals true } requires X <=Int Z [simplification, anywhere]

I think there are three options:

1. The backend can look at side conditions { X #Equals true } #And { Y #Equals true }, and if X impliesBool Y, then remove the { Y #Equals true} side condition. This seems expensive if done without cacheing.
2. The backend can specifically look for integer side conditions it can simplify, including this case.
3. We can figure out a way of writing a rule so that the backend correctly applies it to simplify this situation.

I personally prefer (3), but I can't figure out a rule that the backend will accept.

I've attached a bug-report with the definition which includes all three rules: test.tar.gz

Start with the attached test.tar.gz definition and reproduce the proof to depth 4, focusing on the generated integer side-conditions. Compare the behavior of the three proposed simplification rules and the backend output. Done means identifying a supported way to remove redundant conditions and preventing their growth in long KEVM proofs.