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 | |
parent | 2bf94333ba1f2791b07b9799a87ba0ae987179a1 (diff) |
Return RecoverableModalException when model is not available. (#3283)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 |
2 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 78db1718e..b8f6bf15c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -900,7 +900,12 @@ TheoryModel* TheoryEngine::getBuiltModel() { // If this method was called, we should be in SAT mode, and produceModels // should be true. - AlwaysAssert(d_inSatMode && options::produceModels()); + AlwaysAssert(options::produceModels()); + if (!d_inSatMode) + { + // not available, perhaps due to interuption. + return nullptr; + } // must build model at this point d_curr_model_builder->buildModel(d_curr_model); } 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 |