An example that runs on llvm backend but does not on the Haskell backend.

Guys, I know you are all overloaded with work, over 200 issues! But please take a look at the situation below.

The following K description runs just fine in the llvm backend but either loops or takes quite a while to finish in the Haskell backend.
This example is a simplification of Plutus semantics in K that arose while running the ML Proof Checker. Could you shed some light?

require "domains.md"
module TEST
 imports LIST
 imports K-EQUAL
 imports INT
 imports STRING

 syntax String ::= head(String) [function]
 rule head(S) => substrString(S, 0, 1)
 syntax String ::= tail(String) [function]
 rule tail(S) => substrString(S, 1, lengthString(S))

 syntax List ::= f(String, List) [function]
 rule f(S, L) =>
      #if S ==String ""
      #then (L)
      #else f(tail(S), (L ListItem(head(S))))
      #fi
endmodule

In LLVM:

$ kompile --backend llvm t.k --main-module TEST
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.
$ time krun -cPGM="f(\"ola\", .List)" --depth 0
<k>
  ListItem ( "o" )
  ListItem ( "l" )
  ListItem ( "a" ) ~> .
</k>

real    0m0.990s
user    0m2.462s
sys     0m0.133s

In Haskell:

$ kompile --backend haskell t.k --main-module TEST
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.

$ time krun -cPGM="f(\"ola\", .List)" --depth 0
^Ckore-exec: [12129483] Error (ErrorException):
    Error while communicating with the solver:
        fd:137: hFlush: resource vanished (Broken pipe)
    Solver exit code: -2
Created bug report: kore-exec.tar.gz
[Error] Critical: Backend crashed during rewriting with exit code 1

real    0m13.209s
user    0m16.102s
sys     0m0.606s

Reproduce the example in t.k by compiling it with the LLVM and Haskell backends, then running krun with PGM="f("ola", .List)" and --depth 0. Compare the successful LLVM result with the Haskell backend's long run and solver communication error; done means the Haskell backend terminates and produces the same list output.