diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-24 20:56:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-24 20:56:21 -0500 |
| commit | 78b3f62746e95b915436c6a9bb57dab7be4d4fa4 (patch) | |
| tree | 57c36e4803b1be7919c5d7be0cafe33a60b2fd54 /src/smt/smt_engine.cpp | |
| parent | 7988675ce9666b6f2214b583d42b9fa8be52ae60 (diff) | |
Return choice functions for approximate values in get-value (#3304)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fa318aaf1..305c36d13 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4212,8 +4212,10 @@ Expr SmtEngine::getValue(const Expr& ex) const || resultNode.getType().isSubtypeOf(expectedType), "Run with -t smt for details."); - // ensure it's a constant - Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); + // Ensure it's a constant, or a lambda (for uninterpreted functions), or + // a choice (for approximate values). + Assert(resultNode.getKind() == kind::LAMBDA + || resultNode.getKind() == kind::CHOICE || resultNode.isConst()); if(options::abstractValues() && resultNode.getType().isArray()) { resultNode = d_private->mkAbstractValue(resultNode); |