diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index ffc17d43e..b4cd22830 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -2005,6 +2005,7 @@ public:
                 res = make(commute,pf,comm_equiv);
                 break;
             }
+            case PR_NOT_OR_ELIM:
             case PR_AND_ELIM: {
                 std::vector<ast> rule_ax, res_conc;
                 ast piv = conc(prem(proof,0));