summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/fmf/full_model_check.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/fmf/full_model_check.h')
-rw-r--r--src/theory/quantifiers/fmf/full_model_check.h10
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 732f8be07..a64c33303 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -138,13 +138,15 @@ public:
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
- int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+ int doExhaustiveInstantiation(FirstOrderModel* fm,
+ Node f,
+ int effort) override;
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
- /** process build model */
- bool preProcessBuildModel(TheoryModel* m);
- bool processBuildModel(TheoryModel* m);
+ /** process build model */
+ bool preProcessBuildModel(TheoryModel* m) override;
+ bool processBuildModel(TheoryModel* m) override;
bool useSimpleModels();
};/* class FullModelChecker */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback