diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-01 22:44:40 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-01 22:44:40 +0200 |
| commit | cbcc5124a8f0f17acd981a80c182616cd0a778ff (patch) | |
| tree | 0a77487acde8a9a05762b7dcfe436c76defb1f0b /src/prop/cnf_stream.cpp | |
| parent | 7f85896a9f1c9d3c8f65c53c16fea2156bc4dfab (diff) | |
When proof enabled, disable uf sym break. Add regression.
Diffstat (limited to 'src/prop/cnf_stream.cpp')
| -rw-r--r-- | src/prop/cnf_stream.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f03cc9944..b0b135b04 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -667,7 +667,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated Assert((uint64_t(proof_id) & 0xffffffff00000000llu) == 0 && (assertionTableIndex & 0xffffffff00000000llu) == 0, "proof_id/table_index collision"); d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32); d_assertionTable.push_back(from.isNull() ? node : from); - Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; + Debug("cores") << "; cnf is " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; } else { // We aren't producing proofs or unsat cores; use an invalid proof id. d_proofId = uint64_t(-1); |