Handling Non-Convex Theories Many theories are non-convex Consider the theory of memory and pointers It is not-convex: trueA=A'v sel(upd(M,A,V),A')=sel(M,A) (neither of the dis juncts is entailed individually) For such theories it can be the case that No contradiction is discovered No single equality is discovered - But a disjunction of equalities is discovered We need to propagate disjunction of equalities.. Prof.Necula CS 294-8 Lecture 12 10Prof. Necula CS 294-8 Lecture 12 10 Handling Non-Convex Theories • Many theories are non-convex • Consider the theory of memory and pointers – It is not-convex: true  A = A’  sel(upd(M, A, V), A’) = sel(M, A’) (neither of the disjuncts is entailed individually) • For such theories it can be the case that – No contradiction is discovered – No single equality is discovered – But a disjunction of equalities is discovered • We need to propagate disjunction of equalities …