Closed
Description
This script:
(set-logic ALL)
(declare-datatypes ((Pair 2)) ((par (X Y) ((pair (first X) (second Y))))))
; Uncomment the following line and it works!
; (define-fun x () (Pair Bool Bool) (pair true true))
(assert (= (first (pair true true)) true))
Causes z3 to say:
(error "line 8 column 33: unknown constant pair (Bool Bool) ")
Interestingly, if you uncomment the 6th line with define-fun, it goes through without any complaint.
Metadata
Metadata
Assignees
Labels
No labels