Information

A segmentation fault is thrown when using let within a define-fun.

Reproducible on both 0.6.0 and 0.7.0.

$ z3 test.smt2
sat

$ cvc5 test.smt2
sat

$ bitwuzla test.smt2
Segmentation fault (core dumped)

$ bitwuzla --version
0.7.0

Minimal Reproduction Model

; test.smt2
(set-logic ALL)

(define-fun foo ((x (_ BitVec 4))) (_ BitVec 4)
  (let ((x (bvadd x #b0001))) x)
)

(declare-const input (_ BitVec 4))

(assert (= (foo input) #b0100))
(check-sat)

Edits:

• Simplified/minified minimal reproduction model