equiv_induct: Fix up assumption for $equiv cells in -undef mode.

Before this fix, equiv_induct only assumed that one of the following is
true:

- defined value of A is equal to defined value of B
- A is undefined

This lets through valuations where A is defined, B is undefined, and
the defined (meaningless) value of B happens to match the defined value
of A.  Instead, tighten this up to OR of the following:

- defined value of A is equal to defined value of B, and B is not
  undefined
- A is undefined

1 files changed, 3 insertions, 1 deletions

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index 596c938fc..37aec50cd 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -65,8 +65,10 @@ struct EquivInductWorker
 					int ez_a = satgen.importSigBit(bit_a, step);
 					int ez_b = satgen.importSigBit(bit_b, step);
 					int cond = ez->IFF(ez_a, ez_b);
-					if (satgen.model_undef)
+					if (satgen.model_undef) {
+						cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_b, step)));
 						cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step));
+					}
 					ez_equal_terms.push_back(cond);
 				}
 			}