search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

fix join sort #9

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

(error "line 88 column 60: invalid function application, sort mismatch on argument at position 1")

(and (and (one_1 Root) (not (some_1 (join_1x2 Root parent)))) (forall ((o Atom)) (forall ((d Atom)) (=> (and (in_1 o FSO) (in_1 d Dir)) (=> (subset_1 (a2r_1 o) (join_1x2 (a2r_1 d) entries)) (= (join_1x2 (a2r_1 o) parent) (a2r_1 d)))))))

cause: (declare-fun join_1x2 (Rel1 Rel2) Bool)

jonnybest commented 12 years ago

also (error "line 94 column 70: invalid function application, sort mismatch on argument at position 1")

jonnybest commented 12 years ago

fixed in 5a9f58d0968f34347ba9c2629728e35354c794a4