From 2d33d0ed288841a6a5ee21aa5b253f041deebf10 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 25 Aug 2014 11:38:27 -0400 Subject: [PATCH] Fix Win32 builds. --- src/proof/proof_manager.cpp | 4 ++-- src/prop/cnf_stream.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 0cca16574..87eded8e6 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -174,12 +174,12 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK } else if(options::unsatCores()) { Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff); Debug("cores") << "core input assertion from CnfStream is " << e << std::endl; - Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) << std::endl; + Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl; // Invalid proof rules are currently used for parts of CVC4 that don't // support proofs (these are e.g. unproven theory lemmas) or don't need // proofs (e.g. split lemmas). We can ignore these safely when // constructing unsat cores. - if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) != RULE_INVALID) { + if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) != RULE_INVALID) { // trace dependences back to actual assertions traceDeps(Node::fromExpr(e)); } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 0d133aa13..ad187aa46 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -651,7 +651,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated if(options::proof() || options::unsatCores()) { // Encode the assertion ID in the proof_id to store with generated clauses. uint64_t assertionTableIndex = d_assertionTable.size(); - Assert((uint64_t(proof_id) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 0, "proof_id/table_index collision"); + 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; -- 2.30.2