lone_1 mult not declared

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

lone_1 mult not declared #23

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

the generation of the line

(assert
  (forall ((this Atom)) (=> (in_1 this Interface) (and (forall ((x0 Atom)) (=> (in_1 x0 IID) (lone_1 (join_1x2 (a2r_1 x0) (join_1x3 (a2r_1 this) qi))))) (forall ((x0 Atom)) true))))
)

does not trigger the declaration of lone_1

from com_theorem1.als

jonnybest commented 12 years ago

as of https://github.com/jonnybest/thesisalloy2smt/commit/6a845df6986cf2cf0e1398c08fb569acf2a08705 this does not occur any more. I had missed some term calls to lone_1 without checking arity first.