diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 02:02:07 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 02:02:07 +0000 |
| commit | aad6d724f09fe523d7c1d53e2db959801f28fc3e (patch) | |
| tree | 53eddc4dbe8d24751ccd0a0a54a50bd5b2137627 /src/expr/expr_manager_template.cpp | |
| parent | eee91ecc512e94358a02d2aa155764e4cda2e5fa (diff) | |
Fixing failing test in r521
Adding general support for associative operators in SMT v1 and v2
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 59dbf77e5..8cfd50f08 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -252,6 +252,8 @@ Expr ExprManager::mkVar(const Type& type) { Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { + Assert( metakind::isAssociative(kind), "Illegal kind in mkAssociative" ); + NodeManagerScope nms(d_nodeManager); const unsigned int max = maxArity(kind); const unsigned int min = minArity(kind); |