search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
635 stars 74 forks source link

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

Open SulemanAhmadd opened 8 months ago

SulemanAhmadd commented 8 months ago

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 commented 5 months ago

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

SulemanAhmadd commented 5 months ago

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 commented 5 months ago

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