Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Segmentation fault with fun-rec #6713

Closed
brutalsavage opened this issue May 7, 2023 · 1 comment
Closed

Segmentation fault with fun-rec #6713

brutalsavage opened this issue May 7, 2023 · 1 comment

Comments

@brutalsavage
Copy link

Description: Segmentation fault with func-rec

small code small.smt2 to reproduce:

(declare-fun x () Int)
(declare-fun z () Int)

(define-fun-rec fib-odd ((n Int)) Int
  (ite (<= n 0)
       0
     (ite (= n 1)
          1
        (+ (fib-even (- n 1)) (fib-odd (- n 2))))))

(define-fun-rec fib-even ((n Int)) Int
  (ite (<= n 0)
           0
     (ite (= n 1)
              0
          (+ (fib-odd (- n 1)) (fib-even (- n 2))))))

(assert (= (mod (+ (fib-even x)) 13) z))

(check-sat)

output

(error "line 9 column 28: unknown constant fib-even (Int) ")
Segmentation fault (core dumped)

Note: changing code to define-fun instead of define-fun-rec no longer segfaults

Command: running z3 (6c24a70) with debug build z3 small.smt2

@NikolajBjorner
Copy link
Contributor

these are fuzz bugs for malformed input. It isn't clear spending bandwidth on these helps anybody.
I may be closing such bugs without further comments in the future.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants