diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-12 12:23:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-12 12:23:57 -0500 |
| commit | af135825a60f917711d133828c9fdd6831e2142d (patch) | |
| tree | 20e9b46a027b8f8242901964fa360bb849f640df /src/theory/quantifiers/theory_quantifiers.h | |
| parent | 6b5b926f28b66c3812d77fd234e93b9eee03f71f (diff) | |
Fixes for free variables in assertions (#1762)
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.h')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 4f87f6aae..4bb28fe79 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -58,10 +58,6 @@ class TheoryQuantifiers : public Theory { Node n, std::vector<Node> node_values, std::string str_value) override; - bool ppDontRewriteSubterm(TNode atom) override - { - return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; - } private: void assertUniversal( Node n ); |