diff --git a/integration_test/circt-lec/hw.mlir b/integration_test/circt-lec/hw.mlir
index 92023fa1afdb..361175f90c81 100644
--- a/integration_test/circt-lec/hw.mlir
+++ b/integration_test/circt-lec/hw.mlir
@@ -40,3 +40,28 @@ hw.module @notnot(%in: i1) -> (out: i1) {
 // hw.output
 //  RUN: circt-lec %s -c1=basic -c2=basic -v=false | FileCheck %s --check-prefix=HW_OUTPUT
 //  HW_OUTPUT: c1 == c2
+
+
+hw.module @constZeroZero(%in: i1) -> (o1: i1, o2: i1) {
+  %zero = hw.constant 0 : i1
+  hw.output %zero, %zero : i1, i1
+}
+
+hw.module @xorZeroZero(%in: i1) -> (o1: i1, o2: i1) {
+  %zero = comb.xor bin %in, %in : i1
+  hw.output %zero, %zero : i1, i1
+}
+
+hw.module @constZeroOne(%in: i1) -> (o1: i1, o2: i1) {
+  %zero = hw.constant 0 : i1
+  %one  = hw.constant 1 : i1
+  hw.output %zero, %one : i1, i1
+}
+
+// Equivalent modules with two outputs
+//  RUN: circt-lec %s -c1=constZeroZero -c2=xorZeroZero -v=false | FileCheck %s --check-prefix=TWOOUTPUTS
+//  TWOOUTPUTS: c1 == c2
+
+// Modules with one equivalent and one non-equivalent output
+//  RUN: not circt-lec %s -c1=constZeroZero -c2=constZeroOne -v=false | FileCheck %s --check-prefix=TWOOUTPUTSFAIL
+//  TWOOUTPUTSFAIL: c1 != c2
diff --git a/lib/LogicalEquivalence/Solver.cpp b/lib/LogicalEquivalence/Solver.cpp
index 3757c04e5742..f8f138c3391f 100644
--- a/lib/LogicalEquivalence/Solver.cpp
+++ b/lib/LogicalEquivalence/Solver.cpp
@@ -173,6 +173,8 @@ LogicalResult Solver::constrainCircuits() {
     return failure();
   }
 
+  z3::expr_vector outputTerms(context);
+
   const auto *c1outIt = c1Outputs.begin();
   const auto *c2outIt = c2Outputs.begin();
   for (unsigned i = 0; i < nc1Outputs; i++) {
@@ -182,8 +184,11 @@ LogicalResult Solver::constrainCircuits() {
       return failure();
     }
     // Their ith outputs have to be equivalent.
-    solver.add(*c1outIt++ != *c2outIt++);
+    outputTerms.push_back(*c1outIt++ != *c2outIt++);
   }
 
+  // The circuits are not equivalent iff any of the outputs is not equal
+  solver.add(z3::mk_or(outputTerms));
+
   return success();
 }