projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 795e5ba) | patch
SmtEngine::checkModel() should only be called if the result is sat or unknown because...
authorTim King <taking@cs.nyu.edu>
Tue, 13 Nov 2012 21:48:33 +0000 (21:48 +0000)
committerTim King <taking@cs.nyu.edu>
Tue, 13 Nov 2012 21:48:33 +0000 (21:48 +0000)
commit9e70f04c40674ef5f00b7d07a8529bafe9ff2dfc
treeb59377196037f51c735233bd2fa971f558cf4821tree
parent795e5ba8a1138a371409ac9c8e9da78ce652bb94commit | diff
SmtEngine::checkModel() should only be called if the result is sat or unknown because of incompleteness. Other unknown results are not safe to build models for, timeout, interrupted, etc.
src/smt/smt_engine.cpp diff | blob | history