Add constexpr annotations to help coverity understand constant ... (#2314)

1 files changed, 18 insertions, 16 deletions

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;
               }
             }
           }