diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-16 14:14:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-16 14:14:12 -0500 |
| commit | 2a26c175f602effa857fbd16b07cd7ed0f70f01a (patch) | |
| tree | 2aabce72b42bcce4fc4b60c99e7cbced8a76facb /src/theory/theory_engine.h | |
| parent | 2bf94333ba1f2791b07b9799a87ba0ae987179a1 (diff) | |
Return RecoverableModalException when model is not available. (#3283)
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 701d5cefb..23d3282de 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -751,7 +751,10 @@ public: * response to a check-sat call, and only if produceModels is true. * * If the model is not already built, this will cause this theory engine - * to build to the model. + * to build the model. + * + * If the model is not available (for instance, if the last call to check-sat + * was interrupted), then this returns the null pointer. */ theory::TheoryModel* getBuiltModel(); /** set eager model building |