From 626e3b33bbd5b87a5062db81471c87d0bc4aa4a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= <tomaqa@gmail.com>
Date: Mon, 4 Aug 2025 18:38:15 +0200
Subject: [PATCH] Preferring brace initialization of SMTOption-s and avoiding
 narrowing conversions

---
 src/bin/opensmt.cc              | 11 +++++------
 src/options/SMTConfig.h         |  3 ++-
 src/parallel/opensmtSplitter.cc |  6 +++---
 test/unit/test_Timeout.cc       |  3 +--
 4 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/bin/opensmt.cc b/src/bin/opensmt.cc
index 35e00bdef..c379e9164 100644
--- a/src/bin/opensmt.cc
+++ b/src/bin/opensmt.cc
@@ -324,13 +324,13 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
                 printHelp();
                 exit(0);
             case 'v':
-                res.setOption(SMTConfig::o_verbosity, SMTOption(true), msg);
+                res.setOption(SMTConfig::o_verbosity, SMTOption{true}, msg);
                 break;
             case 'd':
-                res.setOption(SMTConfig::o_dryrun, SMTOption(true), msg);
+                res.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg);
                 break;
             case 'r':
-                if (!res.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg))
+                if (!res.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg))
                     fprintf(stderr, "Error setting random seed: %s\n", msg);
                 else
                     fprintf(stderr, "; Using random seed %d\n", atoi(optarg));
@@ -339,7 +339,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
                 res.setOption(SMTConfig::o_produce_models, SMTOption(true), msg);
                 break;
             case 'i':
-                res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+                res.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg);
                 break;
             case 't': {
                 int64_t timeLimit;
@@ -349,8 +349,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
                     throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()};
                 }
 
-                //+ SMTOption is not defined for long long
-                ok &= res.setOption(SMTConfig::o_time_limit, SMTOption(long(timeLimit)), msg);
+                ok &= res.setOption(SMTConfig::o_time_limit, SMTOption{timeLimit}, msg);
                 break;
             }
             case 'p':
diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h
index 9ce585ed3..8252d7ee4 100644
--- a/src/options/SMTConfig.h
+++ b/src/options/SMTConfig.h
@@ -148,6 +148,7 @@ namespace opensmt {
       SMTOption(int i)   : value(i) {}
       //+ Should also support long representation
       SMTOption(long i)  : SMTOption(static_cast<int>(i)) {}
+      SMTOption(long long i)  : SMTOption(static_cast<long>(i)) {}
       SMTOption(double i): value(i) {}
       SMTOption(const char* s) : value(s) {}
       inline bool isEmpty() const { return value.type == O_EMPTY; }
@@ -964,7 +965,7 @@ namespace opensmt {
 
       void setSimplifyInterpolant(int val) {
           const char* msg;
-          setOption(o_simplify_inter, SMTOption(val), msg);
+          setOption(o_simplify_inter, SMTOption{val}, msg);
       }
 
       int getSimplifyInterpolant() const {
diff --git a/src/parallel/opensmtSplitter.cc b/src/parallel/opensmtSplitter.cc
index f920ba898..6fca95986 100644
--- a/src/parallel/opensmtSplitter.cc
+++ b/src/parallel/opensmtSplitter.cc
@@ -80,16 +80,16 @@ int main( int argc, char * argv[] )
                 break;
             case 'd':
                 const char* msg;
-                c.setOption(SMTConfig::o_dryrun, SMTOption(true), msg);
+                c.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg);
                 break;
             case 'r':
-                if (!c.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg))
+                if (!c.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg))
                     fprintf(stderr, "Error setting random seed: %s\n", msg);
                 else
                     fprintf(stderr, "; Using random seed %d\n", atoi(optarg));
                 break;
             case 'i':
-                c.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+                c.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg);
                 break;
             case 'p':
                 pipe = true;
diff --git a/test/unit/test_Timeout.cc b/test/unit/test_Timeout.cc
index 44b424cc9..99aeaddf7 100644
--- a/test/unit/test_Timeout.cc
+++ b/test/unit/test_Timeout.cc
@@ -163,9 +163,8 @@ class TimeoutTest : public ::testing::Test {
             solver.setTimeLimit(limit_ms);
         } else {
             auto & config = configs[solverIdx];
-            //+ SMTOption is not defined for long long
             [[maybe_unused]]
-            bool rval = config.setOption(SMTConfig::o_time_limit, SMTOption(long(limit_ms.count())), auxMsg);
+            bool rval = config.setOption(SMTConfig::o_time_limit, SMTOption{limit_ms.count()}, auxMsg);
             assert(rval);
         }
     }