added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index fe1fc5137..00e270bd0 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -35,11 +35,11 @@ namespace theory {
 namespace uf {
 
 class UfTermDb;
-class StrongSolverTheoryUf;
+class StrongSolverTheoryUF;
 
 class TheoryUF : public Theory {
 
-  friend class StrongSolverTheoryUf;
+  friend class StrongSolverTheoryUF;
 
 public:
 
@@ -116,7 +116,7 @@ private:
   NotifyClass d_notify;
 
   /** The associated theory strong solver (or NULL if none) */
-  StrongSolverTheoryUf* d_thss;
+  StrongSolverTheoryUF* d_thss;
 
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
@@ -212,7 +212,7 @@ public:
     return &d_equalityEngine;
   }
 
-  StrongSolverTheoryUf* getStrongSolver() {
+  StrongSolverTheoryUF* getStrongSolver() {
     return d_thss;
   }