Skip to content

Commit 55c014c

Browse files
committed
Preferring brace initialization of SMTOption-s and avoiding narrowing conversions
1 parent 8759c79 commit 55c014c

File tree

4 files changed

+13
-12
lines changed

4 files changed

+13
-12
lines changed

src/bin/opensmt.cc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -276,30 +276,30 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
276276
printVersion();
277277
exit(0);
278278
case minUcoreLongOpt:
279-
res.setOption(SMTConfig::o_minimal_unsat_cores, SMTOption(true), msg);
279+
res.setOption(SMTConfig::o_minimal_unsat_cores, SMTOption{true}, msg);
280280
break;
281281
case fullUcoreLongOpt:
282-
res.setOption(SMTConfig::o_print_cores_full, SMTOption(true), msg);
282+
res.setOption(SMTConfig::o_print_cores_full, SMTOption{true}, msg);
283283
break;
284284
}
285285
break;
286286
case 'h':
287287
printHelp();
288288
exit(0);
289289
case 'v':
290-
res.setOption(SMTConfig::o_verbosity, SMTOption(true), msg);
290+
res.setOption(SMTConfig::o_verbosity, SMTOption{true}, msg);
291291
break;
292292
case 'd':
293-
res.setOption(SMTConfig::o_dryrun, SMTOption(true), msg);
293+
res.setOption(SMTConfig::o_dryrun, SMTOption{true}, msg);
294294
break;
295295
case 'r':
296-
if (!res.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg))
296+
if (!res.setOption(SMTConfig::o_random_seed, SMTOption{atoi(optarg)}, msg))
297297
fprintf(stderr, "Error setting random seed: %s\n", msg);
298298
else
299299
fprintf(stderr, "; Using random seed %d\n", atoi(optarg));
300300
break;
301301
case 'i':
302-
res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
302+
res.setOption(SMTConfig::o_produce_inter, SMTOption{true}, msg);
303303
break;
304304
case 't': {
305305
int64_t timeLimit;
@@ -309,7 +309,7 @@ SMTConfig parseCMDLineArgs( int argc, char * argv[ ] )
309309
throw std::invalid_argument{"Invalid argument of time-limit: "s + e.what()};
310310
}
311311

312-
ok &= res.setOption(SMTConfig::o_time_limit, SMTOption(timeLimit), msg);
312+
ok &= res.setOption(SMTConfig::o_time_limit, SMTOption{timeLimit}, msg);
313313
break;
314314
}
315315
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; }
@@ -947,7 +948,7 @@ namespace opensmt {
947948

948949
void setSimplifyInterpolant(int val) {
949950
const char* msg;
950-
setOption(o_simplify_inter, SMTOption(val), msg);
951+
setOption(o_simplify_inter, SMTOption{val}, msg);
951952
}
952953

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