diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-06 14:23:21 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-06 14:23:21 -0600 |
| commit | 55ef1bf844fcaaddc2a3dd299a48670fea017d97 (patch) | |
| tree | 529c011a70aeccbce4b2f4ac503dbede2607213a /src/smt | |
| parent | 61c78314a1519b5e7be1c45ef9f6cee25b3a10b4 (diff) | |
Throw exception instead of warning for approximate models (#3542)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7e18e5a6f..c034f6f23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4647,12 +4647,12 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): generating model" << endl; TheoryModel* m = getAvailableModel("check model"); - // check-model is not guaranteed to succeed if approximate values were used + // check-model is not guaranteed to succeed if approximate values were used. + // Thus, we intentionally abort here. if (m->hasApproximations()) { - Warning() - << "WARNING: running check-model on a model with approximate values..." - << endl; + throw RecoverableModalException( + "Cannot run check-model on a model with approximate values."); } // Check individual theory assertions |