From 1f469ae989f692502d1dc845d51f5319be10311c Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 21 Aug 2018 12:58:05 -0700
Subject: [PATCH] Add constexpr annotations to help coverity understand
 constant ... (#2314)

---
 src/theory/bv/theory_bv.cpp                   |  6 ++--
 .../sygus/ce_guided_single_inv_sol.cpp        | 34 ++++++++++---------
 2 files changed, 22 insertions(+), 18 deletions(-)

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 541b77fe6..1b7eeddac 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -861,9 +861,11 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   }
 
   // Propagate differs depending on the subtheory
-  // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
+  // * bitblaster needs to be left alone until it's done, otherwise it doesn't
+  //   know how to explain
   // * equality engine can propagate eagerly
-  bool ok = true;
+  // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
+  constexpr bool ok = true;
   if (subtheory == SUB_CORE) {
     d_out->propagate(literal);
     if (!ok) {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 2ee120211..e575dff9b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -700,23 +700,25 @@ Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
           Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false );
           Trace("csi-rcons-debug2") << "  - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl;
           std::map< Node, int >::iterator itt = d_rcons_to_id[stn].find( nr );
-          if( itt!= d_rcons_to_id[stn].end() ){
+          if (itt != d_rcons_to_id[stn].end())
+          {
             // if it is not already reconstructed
-            if( d_reconstruct.find( itt->second )==d_reconstruct.end() ){
-              Trace("csi-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
-              bool do_check = true;//getPathToRoot( itt->second );
-              setReconstructed( itt->second, ns );
-              if( do_check ){
-                Trace("csi-rcons-debug") << "...path to root, try reconstruction." << std::endl;
-                d_tmp_fail.clear();
-                Node ret = getReconstructedSolution( d_root_id );
-                if( !ret.isNull() ){
-                  Trace("csi-rcons") << "Sygus solution (after enumeration) is : " << ret << std::endl;
-                  reconstructed = 1;
-                  return ret;
-                }
-              }else{
-                Trace("csi-rcons-debug") << "...no path to root." << std::endl;
+            if (d_reconstruct.find(itt->second) == d_reconstruct.end())
+            {
+              Trace("csi-rcons") << "...reconstructed " << ns << " for term "
+                                 << nr << std::endl;
+              setReconstructed(itt->second, ns);
+              Trace("csi-rcons-debug")
+                  << "...path to root, try reconstruction." << std::endl;
+              d_tmp_fail.clear();
+              Node ret = getReconstructedSolution(d_root_id);
+              if (!ret.isNull())
+              {
+                Trace("csi-rcons")
+                    << "Sygus solution (after enumeration) is : " << ret
+                    << std::endl;
+                reconstructed = 1;
+                return ret;
               }
             }
           }
-- 
2.30.2