Update BDD library and add bvashr test.

tests/data/check_bvsge_bvashr0_16bit.smt2

@@ -0,0 +1,39 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :source |
+Generated by: Mathias Preiner
+Generated on: 2018-04-06
+Application: Verification of invertibility conditions generated in [1].
+Target solver: Boolector, CVC4, Z3
+Publication:
+[1] Solving Quantified Bit-Vectors using Invertibility Conditions
+    Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli
+    To appear in CAV 2018
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun s () (_ BitVec 16))
+(declare-fun t () (_ BitVec 16))
+
+(define-fun min () (_ BitVec 16)
+  (bvnot (bvlshr (bvnot (_ bv0 16)) (_ bv1 16)))
+)
+(define-fun max () (_ BitVec 16)
+  (bvnot min)
+)
+
+(define-fun SC ((s (_ BitVec 16)) (t (_ BitVec 16))) Bool
+(bvsge (bvlshr max s) t)
+)
+
+(assert
+ (not
+  (and
+  (=> (SC s t) (exists ((x (_ BitVec 16))) (bvsge (bvashr x s) t)))
+  (=> (exists ((x (_ BitVec 16))) (bvsge (bvashr x s) t)) (SC s t))
+  )
+ )
+)
+(check-sat)
+(exit)

tests/main.cpp

@@ -73,6 +73,7 @@ TEST_CASE( "Without approximations", "[noapprox]" )
     REQUIRE( SolveWithoutApprox("../tests/data/nlzbe008.smt2") == UNSAT );
     REQUIRE( SolveWithoutApprox("../tests/data/falseAndFalse.smt2") == UNSAT );
     REQUIRE( SolveWithoutApprox("../tests/data/bvshl0.smt2") == SAT );
+    REQUIRE( SolveWithoutApprox("../tests/data/check_bvsge_bvashr0_16bit.smt2") == UNSAT );
 }
 
 TEST_CASE( "With variable approximations", "[variableapprox]" )