Merge branch 'cexp' of gitlab.inria.fr:mavanzin/pwhile into cexp

src/PWhile/InvariantSolver/Naive.hs

@@ -324,7 +324,7 @@ reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
     walkLhs C.Sup {} _ _           = error "InvariantSolver.Naive.reduce: sup on lhs"
 
     walkRhs _                Bot _ = return []
-    -- walkRhs (C.E 0)          _   _ = return []
+    -- walkRhs (C.E 0)          _   _ = return [] // removes valid constraints in recursive calls
     walkRhs (C.E e)          ctx k = k e ctx
     walkRhs (C.Cond g c1 c2) ctx k = branch g walkRhs c1 c2 ctx k
     walkRhs (C.Plus c1 c2)   ctx k = add walkRhs c1 c2 ctx k