The backend does not apply simplification rule, while being unable to prove the claim without it

See the end of the issue for some comments. For now, here are some instructions for reproducing the issue:

a.k

module A
  imports BOOL
  imports INT

  syntax A ::= a(Int) | b(Int) | c(Int)
  rule a(X) => b(X)
      requires p1(X modInt 2)
  rule a(X) => b(X)
      requires true
          andBool notBool p1(X modInt 2)
          andBool p2(X modInt 2)
  rule a(X) => b(X)
      requires true
          andBool notBool p1(X modInt 2)
          andBool notBool p2(X modInt 2)
  rule b(X) => c(X)

  syntax Bool ::= p1(Int)  [function, total, no-evaluators]
  syntax Bool ::= p2(Int)  [function, total, no-evaluators]

  syntax Bool ::= definedModInt(Int, Int)  [function, total]
  rule definedModInt (_:Int, X:Int) => X =/=Int 0

  syntax Int ::= Int "modIntTotal" Int  [function, total, klabel(_modIntTotal_), symbol, left, smt-hook(mod)]
  rule _ modIntTotal 0 => 0
  rule X modIntTotal Y => X modInt Y [concrete, simplification]

  rule X modInt Y => X modIntTotal Y
      requires definedModInt(X, Y)
      [simplification, symbolic]
endmodule

proof.k

module PROOF
  imports A

  claim a(X) => c(X)
endmodule

command line:

kompile a.k --backend haskell && kprove proof.k

Output:

  #Not ( {
      false
    #Equals
      p1 ( X modInt 2 )
    }
  #And
    {
      false
    #Equals
      p2 ( X modInt 2 )
    } )
#And
  #Not ( {
      false
    #Equals
      p1 ( X modInt 2 )
    }
  #And
    {
      true
    #Equals
      p2 ( X modInt 2 )
    } )
#And
  #Not ( {
    true
  #Equals
    p1 ( X modInt 2 )
  } )
#And
  <k>
    a ( X ) ~> _DotVar1 ~> .
  </k>

Some comments:

1. This proof works if the rewrite rules for a use modIntTotal instead of modInt.
2. The above most likely happens because the Haskell backend does not send terms that include partial functions to Z3. By this I mean that it replaces the entire { true #Equals p1 ( X modInt 2 ) } term with a variable V and simply sends V to z3. When using modIntTotal, the backend replaces { true #Equals p1 ( X modIntTotal 2 ) } with { true #Equals V } and sends that to z3, which means that z3 has a chance to notice that the entire constraint is unsat.
3. If I try to prove claim b(X modInt 2) => c(X modIntTotal 2), then the backend DOES apply the simplification rule since it finishes the proof successfully. I'm not sure what to make of that.

Reproduce the issue with the supplied a.k and proof.k files using kompile a.k --backend haskell && kprove proof.k, then inspect how the Haskell backend handles partial-function terms and simplification constraints sent to Z3. Done means the claim a(X) => c(X) proves successfully while retaining the modInt rules.