summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.cpp
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2020-05-26 09:44:51 -0700
committerGitHub <noreply@github.com>2020-05-26 11:44:51 -0500
commit1e6f142d3b309db022edcfd3218adcb146d73dec (patch)
tree81a9074f701d0392f21e3b58e28a978ce5f569e7 /src/api/cvc4cpp.cpp
parent7da96102de1894fb96eccec5315234d7c441f017 (diff)
Fix mismatched iterators (CID 1493892). (#4531)
Issue found by coverity.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r--src/api/cvc4cpp.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 052b62efc..1ea421c4b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2354,7 +2354,7 @@ Sort Grammar::resolve()
addSygusConstructorTerm(dtDecl, consTerm, ntsToUnres);
}
- if (d_allowVars.find(ntSym) != d_allowConst.cend())
+ if (d_allowVars.find(ntSym) != d_allowVars.cend())
{
addSygusConstructorVariables(dtDecl, ntSym.d_expr->getType());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback