Skip to content

Commit 2ebafd3

Browse files
VolodymyrBgcameel
authored andcommitted
fix: Remove unnecessary Expression temporary in CHCSmtLib2Interface
fix: Remove unnecessary Expression temporary in CHCSmtLib2Interface Update CHCSmtLib2Interface.cpp Update CHCSmtLib2Interface.cpp add repeats to external.sh
1 parent 14fcd5d commit 2ebafd3

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

libsmtutil/CHCSmtLib2Interface.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -465,9 +465,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
465465
smtSolverInteractionRequire(isAtom(nameSortPair[0]), "Invalid format of CHC model");
466466
SortPointer varSort = scopedParser.toSort(nameSortPair[1]);
467467
scopedParser.addVariableDeclaration(asAtom(nameSortPair[0]), varSort);
468-
// FIXME: Why Expression here?
469-
Expression arg = scopedParser.toSMTUtilExpression(nameSortPair[0]);
470-
predicateArgs.push_back(arg);
468+
predicateArgs.push_back(scopedParser.toSMTUtilExpression(nameSortPair[0]));
471469
}
472470

473471
auto parsedInterpretation = scopedParser.toSMTUtilExpression(interpretation);
@@ -479,6 +477,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
479477
});
480478

481479
Expression predicate(asAtom(args[1]), predicateArgs, SortProvider::boolSort);
480+
// FIXME: Why do we need to represent the predicate as Expression?
482481
definitions.push_back(predicate == parsedInterpretation);
483482
}
484483
return Expression::mkAnd(std::move(definitions));

0 commit comments

Comments
 (0)