summaryrefslogtreecommitdiff
path: root/src/options/options.h
diff options
context:
space:
mode:
authorGereon Kremer <gkremer@stanford.edu>2021-04-28 21:50:23 +0200
committerGitHub <noreply@github.com>2021-04-28 19:50:23 +0000
commit541e19463a0a5dc44dc97a494ca295aae296091e (patch)
tree823a0959f997b44f7e96c3c320c213601fe19df9 /src/options/options.h
parentfc0512b6d13349a91da5ac6617acebc41cbd238c (diff)
Refactor resource manager options (#6446)
This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.
Diffstat (limited to 'src/options/options.h')
-rw-r--r--src/options/options.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/options.h b/src/options/options.h
index 4d8a979c6..324850c43 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -192,7 +192,7 @@ public:
bool getStatsEveryQuery() const;
bool getStrictParsing() const;
int getTearDownIncremental() const;
- unsigned long getCumulativeTimeLimit() const;
+ uint64_t getCumulativeTimeLimit() const;
bool getVersion() const;
const std::string& getForceLogicString() const;
int getVerbosity() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback