Skip to content

Commit 2329fc7

Browse files
committed
Updated SMTInterpol to 2.5-1252-g82eb3a0
1 parent 7709691 commit 2329fc7

File tree

2 files changed

+3
-2
lines changed

2 files changed

+3
-2
lines changed

trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/Version.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,5 +23,5 @@
2323
* @author Jochen Hoenicke
2424
*/
2525
public interface Version {
26-
public final static String VERSION = "2.5-1251-g3fc5840e";
26+
public final static String VERSION = "2.5-1252-g82eb3a02";
2727
}

trunk/source/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/theory/cclosure/CCProofGenerator.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -564,7 +564,8 @@ private Term addAuxEquality(SymmetricPair<CCTerm> equality) {
564564
Term rhs = equality.getSecond().getFlatTerm();
565565
// to make cc equalities different from la equalities, ensure that rhs is not a
566566
// constant.
567-
if (rhs.getSort().isNumericSort() && rhs instanceof ConstantTerm) {
567+
if (rhs.getSort().isNumericSort() && rhs instanceof ConstantTerm
568+
&& ((ConstantTerm) rhs).getValue().equals(Rational.ZERO)) {
568569
final Term constantTerm = rhs;
569570
rhs = lhs;
570571
lhs = constantTerm;

0 commit comments

Comments
 (0)