1 files changed, 72 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 b/test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
new file mode 100644
index 000000000..1dae93eb5
--- /dev/null
+++ b/test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
@@ -0,0 +1,72 @@
+; COMMAND-LINE: --sygus-inst --no-check-models
+(set-info :smt-lib-version 2.6)
+(set-logic UFNIA)
+(set-info :source |
+Generated by: Mathias Preiner
+Generated on: 2019-03-22
+Application: Verifying bit-vector rewrite rule candidates independent from bit-width.
+Target solver: CVC4, Z3, Vampire
+Publications: "Towards Bit-Width-Independent Proofs in SMT Solvers " by A. Niemetz, M. Preiner, A. Reynolds, Y. Zohar, C. Barrett, and C. Tinelli, CADE-27 (2019).
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun pow2 (Int) Int)
+(declare-fun intand (Int Int Int) Int)
+(declare-fun intor (Int Int Int) Int)
+(declare-fun intxor (Int Int Int) Int)
+(define-fun bitof ((k Int) (l Int) (a Int)) Int (mod (div a (pow2 l)) 2))
+(define-fun int_all_but_msb ((k Int) (a Int)) Int (mod a (pow2 (- k 1))))
+(define-fun intmax ((k Int)) Int (- (pow2 k) 1))
+(define-fun intmin ((k Int)) Int 0)
+(define-fun in_range ((k Int) (x Int)) Bool (and (>= x 0) (<= x (intmax k))))
+(define-fun intudivtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) (- (pow2 k) 1) (div a b) ))
+(define-fun intmodtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
+(define-fun intneg ((k Int) (a Int)) Int (intmodtotal k (- (pow2 k) a) (pow2 k)))
+(define-fun intnot ((k Int) (a Int)) Int (- (intmax k) a))
+(define-fun intmins ((k Int)) Int (pow2 (- k 1)))
+(define-fun intmaxs ((k Int)) Int (intnot k (intmins k)))
+(define-fun intshl ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a (pow2 b)) (pow2 k)))
+(define-fun intlshr ((k Int) (a Int) (b Int)) Int (intmodtotal k (intudivtotal k a (pow2 b)) (pow2 k)))
+(define-fun intashr ((k Int) (a Int) (b Int) ) Int (ite (= (bitof k (- k 1) a) 0) (intlshr k a b) (intnot k (intlshr k (intnot k a) b))))
+(define-fun intconcat ((k Int) (m Int) (a Int) (b Int)) Int (+ (* a (pow2 m)) b))
+(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (pow2 k)))
+(define-fun intmul ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a b) (pow2 k)))
+(define-fun intsub ((k Int) (a Int) (b Int)) Int (intadd k a (intneg k b)))
+(define-fun unsigned_to_signed ((k Int) (x Int)) Int (- (* 2 (int_all_but_msb k x)) x))
+(define-fun intslt ((k Int) (a Int) (b Int)) Bool (< (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun intsgt ((k Int) (a Int) (b Int)) Bool (> (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun intsle ((k Int) (a Int) (b Int)) Bool (<= (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun intsge ((k Int) (a Int) (b Int)) Bool (>= (unsigned_to_signed k a) (unsigned_to_signed k b)) )
+(define-fun pow2_base_cases () Bool (and (= (pow2 0) 1) (= (pow2 1) 2) (= (pow2 2) 4) (= (pow2 3) 8) ) )
+;qf axioms
+(define-fun pow2_ax () Bool pow2_base_cases)
+(define-fun and_ax ((k Int)) Bool true)
+(define-fun or_ax ((k Int)) Bool true)
+(define-fun xor_ax ((k Int)) Bool true)
+
+; helpers
+(define-fun is_bv_width ((k Int)) Bool
+ (and
+  (> k 0)
+  (and_ax k)
+  (or_ax k)
+  (xor_ax k)
+ )
+)
+
+(define-fun is_bv_var ((k Int) (x Int)) Bool (in_range k x))
+
+
+; problem start
+(assert pow2_ax)
+(assert (not (forall ((s Int) (t Int) (k Int))
+  (=>
+   (and (is_bv_var k s) (is_bv_var k t) (is_bv_width k))
+   (= (intshl k (intor k t (intnot k t)) t) (intshl k (intnot k (intlshr k s s)) t))
+  )
+ )
+))
+(set-info :status unknown)
+(check-sat)
+(exit)