From 96e753041dbd0abc86ff0a6404f13d29edcb985d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 3 Mar 2014 02:14:27 +0100 Subject: [PATCH] fixed freduce for Minisat::SimpSolver: use frozen_literal() --- passes/sat/freduce.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 81250b000..746523f82 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -112,13 +112,13 @@ struct FindReducedInputs size_t idx_bits = get_bits(idx); if (sat_pi_uniq_bitvec.size() != idx_bits) { - sat_pi_uniq_bitvec.push_back(ez.literal(stringf("uniq_%d", int(idx_bits)-1))); + sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1))); for (auto &it : sat_pi) ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back()))); } log_assert(sat_pi_uniq_bitvec.size() == idx_bits); - sat_pi[bit] = ez.literal(stringf("pi_%s", log_signal(bit))); + sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit))); ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit])); for (size_t i = 0; i < idx_bits; i++) -- 2.30.2