Added simplified test cases for #1

issues/gh1/gh1-2.smt2

@@ -1,12 +1,12 @@
 (set-logic QF_BV)
 
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-(declare-fun c () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(declare-fun c () (_ BitVec 8))
 
-(assert (bvugt a #x0000A000))
-(assert (bvugt b #x0000A000))
-(assert (bvuge c #xFFFFFFF0))
+(assert (bvugt a #x0A))
+(assert (bvugt b #x0A))
+(assert (bvuge c #xF0))
 
 (assert (= c (bvmul a b)))
 

issues/gh1/gh1-simp.smt2

@@ -0,0 +1,13 @@
+(set-logic QF_BV)
+
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+;;(declare-fun c () (_ BitVec 8))
+
+(assert (bvugt a #x0A))
+(assert (bvugt b #x0A))
+;;(assert (bvuge c #xF0))
+;;(assert (= c (bvmul a b)))
+
+(check-sat)
+;; (get-model)

issues/gh1/gh1.smt2

@@ -1,14 +1,13 @@
 (set-logic QF_BV)
 
-(declare-fun a () (_ BitVec 8))
-(declare-fun b () (_ BitVec 8))
-(declare-fun c () (_ BitVec 8))
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun c () (_ BitVec 32))
 
-(assert (bvugt a #x0A))
-(assert (bvugt b #x0A))
-(assert (bvuge c #xF0))
+(assert (bvugt a #x0000A000))
+(assert (bvugt b #x0000A000))
+(assert (bvuge c #xFFFFFFF0))
 
 (assert (= c (bvmul a b)))
 
 (check-sat)
-;; (get-model)