From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 25 Aug 2014 15:38:27 +0000 (-0400)
Subject: Fix Win32 builds.
X-Git-Tag: cvc5-1.0.0~6646
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d33d0ed288841a6a5ee21aa5b253f041deebf10;p=cvc5.git

Fix Win32 builds.
---

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;