Skype Meeting 03/05/2016¶

Why we need combination of theories, multipication of non-constants

Short Code example:
t1 = x*y;
x' = x;
y'= y;
t2 = x'*y';
assert(t1 != t2);

Solution: t1 = f(x, y)

Work Plan - Meeting 9-11/05/2016¶

Mile-Stones¶

I. Propositional logic MC for FunFrog + OpenSMT2
Tasks (1) - (3)

II. Theories MC for FunFrog + OpenSMT2/Other
Tasks (1) - (3)

III. Theory aware MC for FunFrog + OpenSMT2
Tasks (1) - (4) and (5.5)