word-level 函数：
　Concatenation　　　@　        　　t1@t2@...@tm
　Extraction　　　　　[i:j]　        　　x[31:26]
　left shift　　　　　　<<　        　　0bin0011 << 3 = 0bin0011000
　right shift　　　　　>>　        　　x[24:17] >> 5, another example: 0bin1000 >> 3 = 0bin0001
　sign extension　　BVSX(bv,n)        BVSX(0bin100, 5) = 0bin11100
　Array READ　　　[index]　　        x_arr[t1]
　Array WRITE　　　WITH　　        x_arr WITH [index] := value
    * For extraction terms, say t[i:j], n > i >= j >= 0, where n is the length of t.
    * For Left shift terms, t << k is equal to k 0's appended to t. The length of t << k is n+k.
    * for Right shift terms, say t >> k, the term is equal to the bitvector obtained by k 0's followed by t[n-1:k]. The length of t >> k is n.
bitwise函数：
　Bitwise AND　　     &　　　　          t1 & t2 & ... & tm
　Bitwise OR　　　　|　　　　           t1 | t2 | t3 | ... | tm
　Bitwise NOT　　     ~　　　　          ~t1
　Bitwise XOR　　     BVXOR　　       BVXOR(t1,t2)
　Bitwise NAND　　   BVNAND　        BVNAND(t1,t2)
　Bitwise NOR　　     BVNOR　          BVNOR(t1,t2)
　Bitwise XNOR　      BVXNOR　        BVXNOR(t1,t2)
　
　It is required that all the arguments of bitwise functions have the same length

运算函数
Add                
      BVPLUS   :  BVPLUS(n,t1,t2,...,tm)
Mult                
      BVMULT  :  BVMULT(n,t1,t2)
Subtract          
      BVSUB  :  BVSUB(n,t1,t2)
Unary Minus   
      BVUMINUS  :  BVUMINUS(t1)
Div                  
      BVDIV  :  BVDIV(n,t1,t2), where t1 is the dividend and t2 is the divisor
Signed Div           
      SBVDIV  :  SBVDIV(n,t1,t2), where t1 is the dividend and t2 is the divisor
Modulo                
      BVMOD  :  BVMOD(n,t1,t2), where t1 is the dividend and t2 is the divisor
Signed Modulo    
      SBVMOD  :  SBVMOD(n,t1,t2), where t1 is the dividend and t2 is the divisor

    * the number of output bits has to specified (except unary minus).
    * Inputs t1,t2 ...,tm must be of the same length
    * BVUMINUS(t) is a short-hand for BVPLUS(n,~t,0bin1), where n is the length of t.
    * Bitvector subtraction (BVSUB(n,t1,t2)) is a short-hand for BVPLUS(n,t1,BVUMINUS(t2))

STP的断言　Predicates

Equality                                   =　　　　  t1=t2
Less Than                              BVLT　　  BVLT(t1,t2)
Greater Than                         BVGT         BVGT(t1,t2)
Less Than Or Equal To          BVLE         BVLE(t1,t2)
Greater Than Or Equal To     BVGE        BVGE(t1,t2)

Signed Less Than                           SBVLT     SBVLT(t1,t2)
Signed Greater Than                      SBVGT     SBVGT(t1,t2)
Signed Less Than Or Equal To      SBVLE      SBVLE(t1,t2)
Signed Greater Than Or Equal To  SBVGE    SBVGE(t1,t2)

    * STP requires that in atomic formulas such as x=y, x and y are expressions of the same length. STP accepts Boolean combination of atomic formulas.

QUERY(FALSE);
判定断言是否无解，如果无解则返回Valid，说明确实是FALSE的。如果有解则返回Invalid，表明断言有解。
COUNTEREXAMPLE；
如果返回结果是Invalid，就给出一个具体的例子来说明结果是Invalid.