basic union find for bitvectors

18 files changed, 487 insertions, 35 deletions

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 0624c00f1..5b8e6d7d3 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -4,41 +4,45 @@ TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	concat-merge-0.smt \ 
-	concat-merge-1.smt \ 
-	concat-merge-2.smt \ 
-	concat-merge-3.smt \ 
-	extract-concat-0.smt \ 
-	extract-concat-1.smt \ 
-	extract-concat-2.smt \ 
-	extract-concat-3.smt \ 
-	extract-concat-4.smt \ 
-	extract-concat-5.smt \ 
-	extract-concat-6.smt \ 
-	extract-concat-7.smt \ 
-	extract-concat-8.smt \ 
-	extract-concat-9.smt \ 
-	extract-concat-10.smt \ 
-	extract-concat-11.smt \ 
-	extract-constant.smt \ 
-	extract-extract-0.smt \ 
-	extract-extract-1.smt \ 
-	extract-extract-2.smt \ 
-	extract-extract-3.smt \ 
-	extract-extract-4.smt \ 
-	extract-extract-5.smt \ 
-	extract-extract-6.smt \ 
-	extract-extract-7.smt \ 
-	extract-extract-8.smt \ 
-	extract-extract-9.smt \ 
-	extract-extract-10.smt \ 
-	extract-extract-11.smt \ 
-	extract-whole-0.smt \ 
-	extract-whole-1.smt \ 
-	extract-whole-2.smt \ 
-	extract-whole-3.smt \ 
-	extract-whole-4.smt  
-
+	concat-merge-0.smt \
+	concat-merge-1.smt \
+	concat-merge-2.smt \
+	concat-merge-3.smt \
+	extract-concat-0.smt \
+	extract-concat-1.smt \
+	extract-concat-2.smt \
+	extract-concat-3.smt \
+	extract-concat-4.smt \
+	extract-concat-5.smt \
+	extract-concat-6.smt \
+	extract-concat-7.smt \
+	extract-concat-8.smt \
+	extract-concat-9.smt \
+	extract-concat-10.smt \
+	extract-concat-11.smt \
+	extract-constant.smt \
+	extract-extract-0.smt \
+	extract-extract-1.smt \
+	extract-extract-2.smt \
+	extract-extract-3.smt \
+	extract-extract-4.smt \
+	extract-extract-5.smt \
+	extract-extract-6.smt \
+	extract-extract-7.smt \
+	extract-extract-8.smt \
+	extract-extract-9.smt \
+	extract-extract-10.smt \
+	extract-extract-11.smt \
+	extract-whole-0.smt \
+	extract-whole-1.smt \
+	extract-whole-2.smt \
+	extract-whole-3.smt \
+	extract-whole-4.smt \
+	equality-00.smt \
+	equality-01.smt \
+	equality-02.smt \
+	bv_eq_diamond10.smt
+	
 EXTRA_DIST = $(TESTS)
 
 # synonyms for "check"
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond10.smt b/test/regress/regress0/bv/core/bv_eq_diamond10.smt
new file mode 100644
index 000000000..6d8042512
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond10.smt
@@ -0,0 +1,33 @@
+(benchmark eq_diamond10
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(not (= x0 x9))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond11.smt b/test/regress/regress0/bv/core/bv_eq_diamond11.smt
new file mode 100644
index 000000000..cf9dccf07
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond11.smt
@@ -0,0 +1,35 @@
+(benchmark eq_diamond11
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(not (= x0 x10))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond12.smt b/test/regress/regress0/bv/core/bv_eq_diamond12.smt
new file mode 100644
index 000000000..97f7159c7
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond12.smt
@@ -0,0 +1,37 @@
+(benchmark eq_diamond12
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(not (= x0 x11))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond13.smt b/test/regress/regress0/bv/core/bv_eq_diamond13.smt
new file mode 100644
index 000000000..9e25875e1
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond13.smt
@@ -0,0 +1,39 @@
+(benchmark eq_diamond13
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32])
+(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
+(not (= x0 x12))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond14.smt b/test/regress/regress0/bv/core/bv_eq_diamond14.smt
new file mode 100644
index 000000000..9eae02e30
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond14.smt
@@ -0,0 +1,41 @@
+(benchmark eq_diamond14
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32])
+(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32])
+(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
+(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
+(not (= x0 x13))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond15.smt b/test/regress/regress0/bv/core/bv_eq_diamond15.smt
new file mode 100644
index 000000000..ed28883a5
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond15.smt
@@ -0,0 +1,43 @@
+(benchmark eq_diamond15
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32])
+(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32])
+(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32])
+(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
+(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
+(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14)))
+(not (= x0 x14))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond16.smt b/test/regress/regress0/bv/core/bv_eq_diamond16.smt
new file mode 100644
index 000000000..4e81c3c31
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond16.smt
@@ -0,0 +1,45 @@
+(benchmark eq_diamond16
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32])
+(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32])
+(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32])
+(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32])
+(x15 BitVec[32]) (y15 BitVec[32]) (z15 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
+(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
+(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14)))
+(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15)))
+(not (= x0 x15))))
diff --git a/test/regress/regress0/bv/core/bv_eq_diamond17.smt b/test/regress/regress0/bv/core/bv_eq_diamond17.smt
new file mode 100644
index 000000000..b65e035e5
--- /dev/null
+++ b/test/regress/regress0/bv/core/bv_eq_diamond17.smt
@@ -0,0 +1,47 @@
+(benchmark eq_diamond17
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32])
+(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32])
+(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32])
+(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32])
+(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32])
+(x15 BitVec[32]) (y15 BitVec[32]) (z15 BitVec[32])
+(x16 BitVec[32]) (y16 BitVec[32]) (z16 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
+(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
+(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14)))
+(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15)))
+(or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16)))
+(not (= x0 x16))))
diff --git a/test/regress/regress0/bv/core/equality-00.cvc b/test/regress/regress0/bv/core/equality-00.cvc
new file mode 100644
index 000000000..e02c616ad
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-00.cvc
@@ -0,0 +1,4 @@
+x, y, z : BITVECTOR(32);
+ASSERT(x = y);
+ASSERT(y = z);
+QUERY(x = z);
\ No newline at end of file
diff --git a/test/regress/regress0/bv/core/equality-00.smt b/test/regress/regress0/bv/core/equality-00.smt
new file mode 100644
index 000000000..dabdae5f9
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-00.smt
@@ -0,0 +1,10 @@
+(benchmark B_
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :extrafuns ((z BitVec[32]))
+  :assumption (= x y)
+  :assumption (= y z)
+  :formula (not (= x z))
+)
diff --git a/test/regress/regress0/bv/core/equality-01.cvc b/test/regress/regress0/bv/core/equality-01.cvc
new file mode 100644
index 000000000..e56af23dd
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-01.cvc
@@ -0,0 +1,5 @@
+x, y, z, w: BITVECTOR(32);
+ASSERT(x = y);
+ASSERT(y = z);
+ASSERT(z = w);
+QUERY(x = w);
\ No newline at end of file
diff --git a/test/regress/regress0/bv/core/equality-01.smt b/test/regress/regress0/bv/core/equality-01.smt
new file mode 100644
index 000000000..48506d2b9
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-01.smt
@@ -0,0 +1,12 @@
+(benchmark B_
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :extrafuns ((z BitVec[32]))
+  :extrafuns ((w BitVec[32]))
+  :assumption (= x y)
+  :assumption (= y z)
+  :assumption (= z w)
+  :formula (not (= x w))
+)
diff --git a/test/regress/regress0/bv/core/equality-02.cvc b/test/regress/regress0/bv/core/equality-02.cvc
new file mode 100644
index 000000000..e8f51d61a
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-02.cvc
@@ -0,0 +1,15 @@
+x0, x1, x2, x3 : BITVECTOR(32);
+y0, y1, y2, y3 : BITVECTOR(32);
+
+ASSERT (x0 = x1);
+ASSERT (x1 = x2);
+ASSERT (x2 = x3);
+
+ASSERT (y0 = y1);
+ASSERT (y1 = y2);
+ASSERT (y2 = y3);
+
+ASSERT (x0 = y0);
+
+QUERY (x3 = y3);
+
diff --git a/test/regress/regress0/bv/core/equality-02.smt b/test/regress/regress0/bv/core/equality-02.smt
new file mode 100644
index 000000000..ee011ceb4
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-02.smt
@@ -0,0 +1,20 @@
+(benchmark B_
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x0 BitVec[32]))
+  :extrafuns ((x1 BitVec[32]))
+  :extrafuns ((x2 BitVec[32]))
+  :extrafuns ((x3 BitVec[32]))
+  :extrafuns ((y0 BitVec[32]))
+  :extrafuns ((y1 BitVec[32]))
+  :extrafuns ((y2 BitVec[32]))
+  :extrafuns ((y3 BitVec[32]))
+  :assumption (= x0 x1)
+  :assumption (= x1 x2)
+  :assumption (= x2 x3)
+  :assumption (= y0 y1)
+  :assumption (= y1 y2)
+  :assumption (= y2 y3)
+  :assumption (= x0 y0)
+  :formula (not (= x3 y3))
+)
diff --git a/test/regress/regress0/bv/core/equality-03.cvc b/test/regress/regress0/bv/core/equality-03.cvc
new file mode 100644
index 000000000..d2f18682c
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-03.cvc
@@ -0,0 +1,10 @@
+x0, x1, x2: BITVECTOR(32);
+y0, y1, y2: BITVECTOR(32);
+a0, a1, a2, a3 : BITVECTOR(32);
+
+ASSERT (a0 = x0 AND x0 = a1) XOR (a0 = y0 AND y0 = a1);
+ASSERT (a1 = x1 AND x1 = a2) XOR (a1 = y1 AND y1 = a2);
+ASSERT (a2 = x2 AND x2 = a3) XOR (a2 = y2 AND y2 = a3);
+
+QUERY (a0 = a3);
+
diff --git a/test/regress/regress0/bv/core/equality-03.smt b/test/regress/regress0/bv/core/equality-03.smt
new file mode 100644
index 000000000..4141c7293
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-03.smt
@@ -0,0 +1,27 @@
+(benchmark B_
+  :source {
+Source unknown
+}
+  :status unknown
+  :difficulty { unknown }
+  :category { unknown }
+  :logic QF_BV
+  :extrafuns ((x0 BitVec[32]))
+  :extrafuns ((x1 BitVec[32]))
+  :extrafuns ((x2 BitVec[32]))
+  :extrafuns ((y0 BitVec[32]))
+  :extrafuns ((y1 BitVec[32]))
+  :extrafuns ((y2 BitVec[32]))
+  :extrafuns ((a0 BitVec[32]))
+  :extrafuns ((a1 BitVec[32]))
+  :extrafuns ((a2 BitVec[32]))
+  :extrafuns ((a3 BitVec[32]))
+  :assumption
+(xor (and (= a0 x0) (= x0 a1)) (and (= a0 y0) (= y0 a1)))
+  :assumption
+(xor (and (= a1 x1) (= x1 a2)) (and (= a1 y1) (= y1 a2)))
+  :assumption
+(xor (and (= a2 x2) (= x2 a3)) (and (= a2 y2) (= y2 a3)))
+  :formula
+(not (= a0 a3))
+)
diff --git a/test/regress/regress0/bv/core/equality-04.smt b/test/regress/regress0/bv/core/equality-04.smt
new file mode 100644
index 000000000..78adf0477
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-04.smt
@@ -0,0 +1,25 @@
+(benchmark eq_diamond10
+:status unsat
+:logic QF_BV
+:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32])
+(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32])
+(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32])
+(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32])
+(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32])
+(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32])
+(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32])
+(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32])
+(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32])
+(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32])
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(not (= x0 x9))))