Skip to content

Commit 3e7358f

Browse files
committed
Preferring brace initialization of SMTOption-s and avoiding narrowing conversions
1 parent f0f7b6f commit 3e7358f

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
@@ -316,13 +316,13 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
316316
printHelp();
317317
exit(0);
318318
case 'v':
319-
res.setOption(SMTConfig::o_verbosity, SMTOption(true), msg);
319+
res.setOption(SMTConfig::o_verbosity, SMTOption{true}, msg);
320320
break;
321321
case 'd':
322-
res.setOption(SMTConfig::o_dryrun, SMTOption(true), msg);
322+
res.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg);
323323
break;
324324
case 'r':
325-
if (!res.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg))
325+
if (!res.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg))
326326
fprintf(stderr, "Error setting random seed: %s\n", msg);
327327
else
328328
fprintf(stderr, "; Using random seed %d\n", atoi(optarg));
@@ -331,7 +331,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
331331
res.setOption(SMTConfig::o_produce_models, SMTOption(true), msg);
332332
break;
333333
case 'i':
334-
res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
334+
res.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg);
335335
break;
336336
case 't': {
337337
int64_t timeLimit;
@@ -341,7 +341,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
341341
throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()};
342342
}
343343

344-
ok &= res.setOption(SMTConfig::o_time_limit, SMTOption(timeLimit), msg);
344+
ok &= res.setOption(SMTConfig::o_time_limit, SMTOption{timeLimit}, msg);
345345
break;
346346
}
347347
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; }
@@ -959,7 +960,7 @@ namespace opensmt {
959960

960961
void setSimplifyInterpolant(int val) {
961962
const char* msg;
962-
setOption(o_simplify_inter, SMTOption(val), msg);
963+
setOption(o_simplify_inter, SMTOption{val}, msg);
963964
}
964965

965966
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)