diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-19 11:13:40 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-19 11:13:40 -0400 |
| commit | e314cee5558babad33e5c8228c74701abc0106cc (patch) | |
| tree | 36263999b27cf6d32b14ba721b6a6ccd7c5bb689 /src/theory/model.cpp | |
| parent | d0ec84da973d3ba7054b61fd620a1eba0d459a48 (diff) | |
Minor fix for --no-condense-function-values
Diffstat (limited to 'src/theory/model.cpp')
| -rw-r--r-- | src/theory/model.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 234b137c8..840c8bc3a 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -53,8 +53,10 @@ Node TheoryModel::getValue(TNode n) const { Node nn = d_substitutions.apply(n); //get value in model nn = getModelValue(nn); - //normalize - nn = Rewriter::rewrite(nn); + if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { + //normalize + nn = Rewriter::rewrite(nn); + } return nn; } |