From 525cc5431a01dac991df3839c5f15729dd91de57 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 21 Feb 2011 04:26:59 +0000
Subject: [PATCH] A new test case for the special unconstrained extract
 handling.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1153 e59a4935-1847-0410-ae03-e826735625c1
---
 unit_test/eqConcat.smt2 | 45 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 unit_test/eqConcat.smt2

diff --git a/unit_test/eqConcat.smt2 b/unit_test/eqConcat.smt2
new file mode 100644
index 0000000..45d9adc
--- /dev/null
+++ b/unit_test/eqConcat.smt2
@@ -0,0 +1,45 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 24))
+(declare-fun v1 () (_ BitVec 24))
+(declare-fun v2 () (_ BitVec 24))
+(declare-fun v3 () (_ BitVec 24))
+
+
+; The
+
+;  1107176:(EQ 
+;    119800:0x00000001
+;    1107174:(BVCONCAT 
+;      119164:0x00000
+;      1107170:(BVCONCAT 
+;        1107166:(BVEXTRACT 
+;          985666:(BVEXTRACT 
+;            985530:unconstrained_36910
+;            120104:0x00000007
+;            118910:0x00000000)
+;          213036:0x00000003
+;          118910:0x00000000)
+;        985668:(BVEXTRACT 
+;          985530:unconstrained_36910
+;          119266:0x0000000F
+;          120112:0x00000008))))
+
+
+(assert  
+	(=	(_ bv1 24)
+		( concat 	
+				(_ bv0 12)				
+				( concat 	
+					((_ extract 3 0) ((_ extract 7 0) v0))
+					((_ extract 15 8) v0)
+				)
+		)
+	)
+)
+
+(check-sat)
+(exit)
+
-- 
2.47.3