aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/bv1.log
diff options
context:
space:
mode:
Diffstat (limited to 'unit-tests/bv1.log')
-rw-r--r--unit-tests/bv1.log12
1 files changed, 12 insertions, 0 deletions
diff --git a/unit-tests/bv1.log b/unit-tests/bv1.log
new file mode 100644
index 0000000..fc101e2
--- /dev/null
+++ b/unit-tests/bv1.log
@@ -0,0 +1,12 @@
+1:(input ((not #1:(= a a))))
+2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a)])))
+3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8)))) 2 2)
+4:(equiv2 (#1 (not #4)) 3)
+5:(resolution ((not #4)) 1 4)
+6:(not_and ((not #5) (not #6)) 5)
+7:(equiv_neg1 (#5 (not #7)))
+8:(equiv_neg2 (#5 #7))
+9:(resolution ((not #6)) 7 8 6)
+10:(equiv_neg1 (#6 (not #8)))
+11:(equiv_neg2 (#6 #8))
+12:(resolution () 10 11 9)