Incompatible with z3 (4.8.12-3.1) version shipped in Debian Bookworm

[SulemanAhmadd]

Hi! I have noticed that the current version of Rosette is not compatible with z3 4.8.12-3.1 package shipped in debian (stable) bookworm.

Specifically, Rosette SMT decoder is unable to recognize 'mod and 'div symbols returned by the z3 solver when using modulo arithmetic on symbolic terms.

(modulo (<some-symbolic-value>) 100)

Unrecognized symbol:  'mod

The log trace refers to failure to decode z3 output:

racket/8.7/pkgs/rosette/rosette/solver/smt/dec.rkt:99:2: inline
racket/8.7/pkgs/rosette/rosette/solver/smt/dec.rkt:25:0: decode-model
racket/8.7/pkgs/rosette/rosette/solver/smt/cmd.rkt:62:0: decode
racket/8.7/pkgs/rosette/rosette/solver/smt/base-solver.rkt:95:0: solver-check
racket/8.7/pkgs/rosette/rosette/query/core.rkt:27:0: ∃-solve

[sorawee]

Could you try #279 and see if it fixes your issue?

[SulemanAhmadd]

I did not get a chance to debug in depth yet but branch z3-bump-4-12-6 is giving a runtime error:

error writing to stream port
  system error: Broken pipe; errno=32
  context...:
.../smt/env.rkt:78:0: ref-expr!
   .../match/compiler.rkt:548:40: f26
   .../smt/env.rkt:78:0: ref-expr!
   .../match/compiler.rkt:548:40: f26
   .../smt/env.rkt:78:0: ref-expr!
   .../match/compiler.rkt:548:40: f26
   .../smt/env.rkt:78:0: ref-expr!
   .../match/compiler.rkt:548:40: f26
   .../smt/env.rkt:78:0: ref-expr!
   .../match/compiler.rkt:548:40: f26
   .../smt/env.rkt:78:0: ref-expr!
   .../match/compiler.rkt:548:40: f26
   .../smt/env.rkt:78:0: ref-expr!
   .../smt/cmd.rkt:25:0: encode
   .../smt/base-solver.rkt:95:0: solver-check
   .../query/core.rkt:27:0: ∃-solve

[sorawee]

Could you provide a minimal, complete example that triggers this issue?