diff --git a/src/main/scala/lazabs/horn/symex/Symex.scala b/src/main/scala/lazabs/horn/symex/Symex.scala
index 821b6a83..efe8834c 100644
--- a/src/main/scala/lazabs/horn/symex/Symex.scala
+++ b/src/main/scala/lazabs/horn/symex/Symex.scala
@@ -407,7 +407,7 @@ abstract class Symex[CC](iClauses:    Iterable[CC])(
   // true if cuc = "FALSE :- c" and c is satisfiable, false otherwise.
   private def hasContradiction(cuc:          UnitClause,
                                proverStatus: ProverStatus.Value): Boolean = {
-    ((cuc.rs.pred == HornClauses.FALSE) || (!cuc.isPositive)) &&
+    ((cuc.rs.pred == HornClauses.FALSE) || (!cuc.isPositive && cuc.rs.pred == HornClauses.FALSE)) &&
     (proverStatus match { // check if cuc constraint is satisfiable
       case ProverStatus.Valid | ProverStatus.Sat     => true
       case ProverStatus.Invalid | ProverStatus.Unsat => false