Fixes for shared term normalization in replay for constraint construction.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 795798450..0e0b35020 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -96,6 +96,13 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+class Comparison;
+}
+}
+}
+namespace CVC4 {
+namespace theory {
+namespace arith {
 
 /**
  * Logs the types of different proofs. 
@@ -448,6 +455,7 @@ private:
   void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation);
 
 
+
   class ConstraintRuleCleanup {
   public:
     inline void operator()(ConstraintRule* crp){
@@ -517,6 +525,8 @@ private:
 
 public:
 
+  static ConstraintType constraintTypeOfComparison(const Comparison& cmp);
+
   inline ConstraintType getType() const {
     return d_type;
   }