From d95fe7675e20eaee86b8e804469e6db83265a005 Mon Sep 17 00:00:00 2001
From: Clark Barrett <clarkbarrett@google.com>
Date: Tue, 21 Apr 2015 16:34:15 -0700
Subject: Changes needed to compile at Google, plus some bug fixes from Google.

---
 src/theory/bv/bitblaster_template.h | 2 +-
 src/theory/bv/lazy_bitblaster.cpp   | 2 +-
 src/theory/bv/theory_bv.cpp         | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'src/theory/bv')

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 79434102e..d4d7bc04c 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -170,7 +170,7 @@ public:
   void storeBBAtom(TNode atom, Node atom_bb);
   bool hasBBAtom(TNode atom) const; 
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
-  ~TLazyBitblaster();
+  ~TLazyBitblaster() throw();
   /** 
    * Pushes the assumption literal associated with node to the SAT
    * solver assumption queue. 
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index fbebcd952..080f23143 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -62,7 +62,7 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
   d_abstraction = abs; 
 }
 
-TLazyBitblaster::~TLazyBitblaster() {
+TLazyBitblaster::~TLazyBitblaster() throw() {
   delete d_cnfStream;
   delete d_nullRegistrar;
   delete d_nullContext;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 08fe5f2e9..9dcd5ac62 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -576,8 +576,8 @@ Node TheoryBV::ppRewrite(TNode t)
   } else if( res.getKind() == kind::EQUAL &&
       ((res[0].getKind() == kind::BITVECTOR_PLUS &&
         RewriteRule<ConcatToMult>::applies(res[1])) ||
-       res[1].getKind() == kind::BITVECTOR_PLUS &&
-       RewriteRule<ConcatToMult>::applies(res[0]))) {
+       (res[1].getKind() == kind::BITVECTOR_PLUS &&
+	RewriteRule<ConcatToMult>::applies(res[0])))) {
     Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
       RewriteRule<ConcatToMult>::run<false>(res[0]) :
       RewriteRule<ConcatToMult>::run<true>(res[1]);
@@ -747,8 +747,8 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
   d_staticLearnCache.insert(in);
     
   if (in.getKind() == kind::EQUAL) {
-    if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL ||
-       in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){
+    if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
+       (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
       TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
 
-- 
cgit v1.2.3