diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala index 55888023dce4ce723b9abc6b242fb6f49aa4dd56..66887e0fcffa3f425cd2a811f11308979a03ec68 100644 --- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala +++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala @@ -191,7 +191,7 @@ trait TemplateGenerator { self: Templates => val rb = rec(pathVar, exprOps.replace(Map(i.toVariable -> newExpr), b), pol) rb - case n @ Not(e) if n.getType == BooleanType => + case n @ Not(e) => Not(rec(pathVar, e, pol.map(!_))) case i @ Implies(lhs, rhs) =>