diff options
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 |