From a1a0abf52afe397e11b63bfc67e82aaf7bf9f498 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Mon, 27 Jul 2020 18:28:01 +0200 Subject: 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 --- passes/equiv/equiv_induct.cc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'passes') 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); } } -- cgit v1.2.3