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 weird errors #8

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

(error "line 64 column 80: unknown function/constant")

63 (assert 64 (forall ((this Atom)) (=> (in_1 this FSO) (lone_1 (join1x2 (a2r_1 this) parent)))) 65 )

declarations: (declare-fun in_1 (Atom Rel1) Bool) (declare-fun parent () Rel2)) (declare-fun join_1x2 (Rel1 Rel2) Bool) (declare-fun a2r_1 (Atom) Rel1) (declare-fun lone_1 (Rel1) Bool) (declare-fun FSO () Rel1)

jonnybest commented 12 years ago

this was caused by old notation: join1x2 <<-->> join_1x2

fixed in 5784c413de0de10c498358baec719263c208cedb