Fix compiler warnings (#1959)

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 3a27fca25a768356968006d895a71994e5384771..f8601af15ee06d1dcd56b7e76d720fbc84bb79b2 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -43,7 +43,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 44 "${template}"
+#line 47 "${template}"
 
 namespace CVC4 {
 
@@ -609,7 +609,7 @@ private:
 
 ${getConst_instantiations}
 
-#line 549 "${template}"
+#line 613 "${template}"
 
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();

diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index b1170b42c5b34632974800e98b30a10dca00a1ed..49ed92deeefceb87475127ac7263a01ca95b5252 100644 (file)
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -8,7 +8,7 @@ theory THEORY_FP ::CVC4::theory::fp::TheoryFp "theory/fp/theory_fp.h"
 typechecker "theory/fp/theory_fp_type_rules.h"
 rewriter ::CVC4::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h"
 
-properties check propagate
+properties check
 
 # Theory content goes here.
 

diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 6234ab8ad4c57a459558e8c014501eae3a7e1c56..832fc64427fc39f3b612aed4c54baf2b9e0cb731 100644 (file)
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -43,11 +43,11 @@ class TheoryFp : public Theory {
   void preRegisterTerm(TNode node) override;
   void addSharedTerm(TNode node) override;
 
-  Node ppRewrite(TNode node);
+  Node ppRewrite(TNode node) override;
 
   void check(Effort) override;
 
-  bool needsCheckLastEffort() { return true; }
+  bool needsCheckLastEffort() override { return true; }
   Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m) override;
 

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index f502ad547f1110cf80606ca0341a2e53df086f2f..496066ebce39e6d63f9b732c30a26b358ecce69a 100644 (file)
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -862,12 +862,12 @@ namespace constantFold {
   {
     Assert(node.getKind() == kind::ROUNDINGMODE_BITBLAST);
 
-    RoundingMode arg0(node[0].getConst<RoundingMode>());
     BitVector value;
 
 #ifdef CVC4_USE_SYMFPU
     /* \todo fix the numbering of rounding modes so this doesn't need
      * to call symfpu at all and remove the dependency on fp_converter.h #1915 */
+    RoundingMode arg0(node[0].getConst<RoundingMode>());
     switch (arg0)
     {
       case roundNearestTiesToEven:

diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index 91ae3e1d657791446c7ebabf586c7728fbf712ab..3daf449fbbb11daa2675bf5090111aacca641ebc 100644 (file)
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -45,7 +45,7 @@ ${mk_type_enumerator_type_constant_cases}
     }
     Unreachable();
 ${mk_type_enumerator_cases}
-#line 47 "${template}"
+#line 49 "${template}"
   default:
     {
       stringstream ss;