-
Notifications
You must be signed in to change notification settings - Fork 1.5k
Closed
Description
For this benchmark:
(set-logic QF_ABV)
(define-fun s0 () (Array (_ BitVec 2) (_ BitVec 2)) ((as const (Array (_ BitVec 2) (_ BitVec 2))) #b00))
(check-sat)
z3 says:
(error "line 2 column 102: unknown constant const ((_ BitVec 2)) (Array (_ BitVec 2) (_ BitVec 2)) ")
sat
If you get rid of set-logic
or use (set-logic ALL)
, the error
isn't produced.
I think the const
should be available as a constant regardless of the logic selection. (As a reference, cvc5
doesn't issue any complaints.)
Metadata
Metadata
Assignees
Labels
No labels