Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index f343848d8..3bfb7fdc5 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -90,7 +90,7 @@ class EqualityTypeRule {
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
 
-      if ( lhsType == booleanType ) {
+      if ( lhsType == booleanType && rhsType == booleanType ) {
         throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)");
       }
     }