diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-16 11:23:54 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 09:23:54 -0800 |
commit | d15d44b3c91b5be2c19adac292f137d2a67eb848 (patch) | |
tree | 67f8cac1485c833970929ab10e216a1d69e8b48d /src/printer/smt2/smt2_printer.cpp | |
parent | 5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb (diff) |
Fix evaluator for non-evaluatable nodes (#3575)
This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.
This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
0 files changed, 0 insertions, 0 deletions