From d02a3c08b7632b495c5d0b41e85868172b123251 Mon Sep 17 00:00:00 2001
From: Karlheinz Friedberger <kfriedberger@gmail.com>
Date: Mon, 5 Feb 2024 20:51:38 +0100
Subject: [PATCH] #357: replace check for boolean constants with direct pointer
 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.
---
 .../sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java
index 27d21cbc46..5febf59fdc 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java
@@ -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