Skip to content

Commit

Permalink
sosy-lab#357: replace check for boolean constants with direct pointer…
Browse files Browse the repository at this point in the history
… comparison.

Z3 uses internal formula hashing,
thus there should not be multiple pointers to the same boolean constants.

This reduces the number of JNI calls for some simple cases.
  • Loading branch information
kfriedberger committed Feb 12, 2024
1 parent e396610 commit d02a3c0
Showing 1 changed file with 2 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -152,12 +152,12 @@ protected Long implication(Long pBits1, Long pBits2) {

@Override
protected boolean isTrue(Long pParam) {
return isOP(z3context, pParam, Z3_decl_kind.Z3_OP_TRUE);
return z3true.equals(pParam);
}

@Override
protected boolean isFalse(Long pParam) {
return isOP(z3context, pParam, Z3_decl_kind.Z3_OP_FALSE);
return z3false.equals(pParam);
}

@Override
Expand Down

0 comments on commit d02a3c0

Please sign in to comment.