Unsound rewrite when using requires with partial functions

versions:

$ kompile --version
K version:    v5.6.122-0-g77b76f004a-dirty
Build date:   Thu Jun 08 22:29:39 EEST 2023

$ kore-exec --version
Kore version 0.60.0.0
Git:
  revision:     f7a90ba41aa98d79f400099e2a27156e07543540
  branch:       HEAD
  last commit:  Fri May 5 08:23:49 2023 -0600

To reproduce:
a.k

module A
  imports INT
  imports BOOL

  syntax KItem ::= "a"
  rule I:Int => a requires 10 /Int I <Int 0
  rule I:Int => a requires 10 /Int I >=Int 0
endmodule

spec.k

module SPEC
  imports A
  claim _Value:Int => a
endmodule

Command line:

$ kompile a.k --backend haskell && kprove spec.k

The proof passes, although the claim should fail when _Value is 0.

Note that the Haskell backend sends partial functions to z3 (i.e. it sends things like 10 /Int I < 0) without attempting to translate them properly - I think that Z3 division is undefined in the sense that it can be ANY value, while the K division is undefined in the sense that it has NO value.

Start by reproducing the issue with a.k, spec.k, kompile a.k --backend haskell, and kprove spec.k. Then inspect the Haskell backend's handling of partial functions sent to Z3 and compare it with K's undefined-function semantics. Done means the claim no longer passes for the value 0 and the behavior is covered by a regression test.