Skip to content
Snippets Groups Projects
Commit 914e24f9 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

ADTSplit should not care about witnesses

parent c9358c44
No related branches found
No related tags found
No related merge requests found
......@@ -22,7 +22,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
val cct = CaseClassType(ccd, tpes)
val toSat = And(p.pc, CaseClassInstanceOf(cct, Variable(id)))
val toSat = And(removeWitnesses(sctx.program)(p.pc), CaseClassInstanceOf(cct, Variable(id)))
val isImplied = solver.solveSAT(toSat) match {
case (Some(false), _) => true
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment