You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As suggested by Nikolaj Bjorner in an e-mail exchange, we should define constant empty sets for every type used in the spec and refer to them instead, as shown below for integers.
(define-const emptyIntSet (Array Int Bool) ((as const (Array Int Bool)) false))
(declare-const set1 (Array Int Bool))
(assert (= set1 emptyIntSet))
The text was updated successfully, but these errors were encountered:
In the initial version of the arrays encoding, every set declaration is followed by an equality to a new empty set, as shown below.
As suggested by Nikolaj Bjorner in an e-mail exchange, we should define constant empty sets for every type used in the spec and refer to them instead, as shown below for integers.
The text was updated successfully, but these errors were encountered: