Skip to content

Commit becc248

Browse files
committed
Preferring brace initialization of SMTOption-s and avoiding narrowing conversions
1 parent c2b81b8 commit becc248

File tree

4 files changed

+11
-10
lines changed

4 files changed

+11
-10
lines changed

src/bin/opensmt.cc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -318,13 +318,13 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
318318
printHelp();
319319
exit(0);
320320
case 'v':
321-
res.setOption(SMTConfig::o_verbosity, SMTOption(true), msg);
321+
res.setOption(SMTConfig::o_verbosity, SMTOption{true}, msg);
322322
break;
323323
case 'd':
324-
res.setOption(SMTConfig::o_dryrun, SMTOption(true), msg);
324+
res.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg);
325325
break;
326326
case 'r':
327-
if (!res.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg))
327+
if (!res.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg))
328328
fprintf(stderr, "Error setting random seed: %s\n", msg);
329329
else
330330
fprintf(stderr, "; Using random seed %d\n", atoi(optarg));
@@ -333,7 +333,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
333333
res.setOption(SMTConfig::o_produce_models, SMTOption(true), msg);
334334
break;
335335
case 'i':
336-
res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
336+
res.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg);
337337
break;
338338
case 't': {
339339
int64_t timeLimit;
@@ -343,7 +343,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
343343
throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()};
344344
}
345345

346-
ok &= res.setOption(SMTConfig::o_time_limit, SMTOption(timeLimit), msg);
346+
ok &= res.setOption(SMTConfig::o_time_limit, SMTOption{timeLimit}, msg);
347347
break;
348348
}
349349
case 'p':

src/options/SMTConfig.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,7 @@ namespace opensmt {
148148
SMTOption(int i) : value(i) {}
149149
//+ Should also support long representation
150150
SMTOption(long i) : SMTOption(static_cast<int>(i)) {}
151+
SMTOption(long long i) : SMTOption(static_cast<long>(i)) {}
151152
SMTOption(double i): value(i) {}
152153
SMTOption(const char* s) : value(s) {}
153154
inline bool isEmpty() const { return value.type == O_EMPTY; }
@@ -960,7 +961,7 @@ namespace opensmt {
960961

961962
void setSimplifyInterpolant(int val) {
962963
const char* msg;
963-
setOption(o_simplify_inter, SMTOption(val), msg);
964+
setOption(o_simplify_inter, SMTOption{val}, msg);
964965
}
965966

966967
int getSimplifyInterpolant() const {

src/parallel/opensmtSplitter.cc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -80,16 +80,16 @@ int main( int argc, char * argv[] )
8080
break;
8181
case 'd':
8282
const char* msg;
83-
c.setOption(SMTConfig::o_dryrun, SMTOption(true), msg);
83+
c.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg);
8484
break;
8585
case 'r':
86-
if (!c.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg))
86+
if (!c.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg))
8787
fprintf(stderr, "Error setting random seed: %s\n", msg);
8888
else
8989
fprintf(stderr, "; Using random seed %d\n", atoi(optarg));
9090
break;
9191
case 'i':
92-
c.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
92+
c.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg);
9393
break;
9494
case 'p':
9595
pipe = true;

src/unsatcores/UnsatCoreBuilder.cc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ SMTConfig UnsatCoreBuilder::Minimize::makeSmtSolverConfig() const {
157157
assert(not newConfig.produce_inter());
158158

159159
char const * msg = "ok";
160-
newConfig.setOption(SMTConfig::o_produce_models, SMTOption(false), msg);
160+
newConfig.setOption(SMTConfig::o_produce_models, SMTOption{false}, msg);
161161
assert(not newConfig.produce_models());
162162

163163
return newConfig;

0 commit comments

Comments
 (0)