Fix ite* rewrite bug.

jamestiotio · Dec 6, 2021 · 9d14d44 · 9d14d44
1 parent 3d84cdc
commit 9d14d44
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/rosette/base/core/polymorphic.rkt b/rosette/base/core/polymorphic.rkt
@@ -152,7 +152,7 @@
   (match* ((car p) (cdr p))
     [(a (expression (== ite) a x _)) (cons a x)]
     [(a (expression (== ite) (expression (== @!) a) _ x)) (cons a x)]
-    [((expression (== @!) a) (expression (== ite) a _ x)) (cons a x)]
+    [((and (expression (== @!) a) !a) (expression (== ite) a _ x)) (cons !a x)]
     [(_ _) p]))