24 lines
945 B
C++
24 lines
945 B
C++
kind::IFF was removed in CVC4 1.6
|
|
--- src/Mixfix/variableGenerator.cc.orig 2018-09-17 10:44:35 UTC
|
|
+++ src/Mixfix/variableGenerator.cc
|
|
@@ -312,18 +312,7 @@ VariableGenerator::dagToCVC4(DagNode* dag)
|
|
//
|
|
case SMT_Symbol::EQUALS:
|
|
{
|
|
- //
|
|
- // Bizarrely CVC4 requires the IFF be used for Boolean equality so we need to
|
|
- // check the SMT type associated with our first argument sort to catch this case.
|
|
- //
|
|
- Sort* domainSort = s->getOpDeclarations()[0].getDomainAndRange()[0];
|
|
- SMT_Info::SMT_Type smtType = smtInfo.getType(domainSort);
|
|
- if (smtType == SMT_Info::NOT_SMT)
|
|
- {
|
|
- IssueWarning("term " << QUOTE(dag) << " does not belong to an SMT sort.");
|
|
- goto fail;
|
|
- }
|
|
- return exprManager->mkExpr(((smtType == SMT_Info::BOOLEAN) ? kind::IFF : kind::EQUAL), exprs[0], exprs[1]);
|
|
+ return exprManager->mkExpr(kind::EQUAL, exprs[0], exprs[1]);
|
|
}
|
|
case SMT_Symbol::NOT_EQUALS:
|
|
{
|