Add

test/regress/cli/regress0/arrays/dd_ios_t1_norm_op.smt2

@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(assert (= (store a (+ i 2) 0) (store (store (store (store (store (store a (+ i 3) 0) (+ i 2) 1) (+ i 1) 0) i 0) (+ i 5) 0) i 0)))
+(check-sat)

test/regress/cli/regress0/arrays/dd_storecomm_norm_op.smt2

@@ -0,0 +1,14 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () (Array Int Int))
+(declare-fun e () Int)
+(declare-fun e1 () Int)
+(declare-fun e3 () Int)
+(declare-fun e35 () Int)
+(declare-fun e36 () Int)
+(declare-fun e37 () Int)
+(declare-fun e38 () Int)
+(declare-fun e6 () Int)
+(declare-fun s ((Array Int Int) (Array Int Int)) Int)
+(assert (distinct (select (store (store (store (store (store (store (store (store a 1 e) 8 e1) 17 e3) 3 e35) 9 e36) 4 e37) 2 e38) 0 e6) (s a a)) (select (store (store (store (store (store (store (store (store (store a 17 e3) 4 e37) 2 e38) 9 e36) 8 e1) 3 e35) 0 0) 1 e) 0 e6) (s a a))))
+(check-sat)

test/regress/cli/regress0/bv/div-zero-eval-tests.smt2

@@ -0,0 +1,10 @@
+; EXPECT: unsat
+(set-logic ALL)
+
+(assert (or
+
+(not (= (bvudiv #b1010 #b0000) #b1111))
+(not (= (bvurem #b1010 #b0000) #b1010))
+
+))
+(check-sat)

test/regress/cli/regress0/datatypes/dt-param-simple-unsat.smt2

@@ -0,0 +1,9 @@
+; DISABLE-TESTER: cpc
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ( (List 1) ) (
+(par ( X ) ( (nil) (cons (head X) (tail (List X)))))
+))
+(declare-fun x () (List Int))
+(assert (= (cons 0 x) (as nil (List Int))))
+(check-sat)

test/regress/cli/regress0/datatypes/eq-clash-rec-find.smt2

@@ -0,0 +1,10 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatype Tree ((node (data Int) (left Tree) (right Tree)) (leaf)))
+(declare-fun L () Tree)
+(declare-fun x () Int)
+(declare-fun y () Int)
+; non-trivial instance of dt-cons-eq-clash reconstruction for nested values
+(assert (= (node x (node y leaf leaf) (node y (node 5 leaf leaf) L))
+           (node x (node 5 leaf L) (node 2 (node 3 leaf L) L))))
+(check-sat)

test/regress/cli/regress0/lambda-shadow-sem.smt2

@@ -0,0 +1,9 @@
+; DISABLE-TESTER: dump
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "All formal arguments to defined functions must be unique"
+; EXPECT: All formal arguments to defined functions must be unique
+; EXIT: 1
+(set-logic ALL)
+(define-fun P ((x Int) (x Int)) Bool (= x 0))
+(assert (P 0 1))
+(check-sat)

test/regress/cli/regress0/proofs/dd_int_check_bvnot_lam_value_norm.smt2

@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(define-fun l ((s Int) (x Int) (t Int) (x0 Int)) Bool (= x 0))
+(define-fun n ((s Int) (t Int) (x0 Int)) Bool (and false (l 0 0 0 0)))
+(assert (n 0 0 0))
+(check-sat)

test/regress/cli/regress0/proofs/dd_issue3481_beta_red.smt2

@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ADTLIRA)
+(define-fun i ((y Int)) Bool false)
+(define-fun d ((x Int)) Bool (or (i x)))
+(assert (exists ((y Int)) (d y)))
+(check-sat)

test/regress/cli/regress0/proofs/exists-shadow-simple.smt2

@@ -0,0 +1,4 @@
+; EXPECT: unsat
+(set-logic ADTLIRA)
+(assert (exists ((k Int) (k Int)) false))
+(check-sat)

test/regress/cli/regress0/proofs/shadow_quant.smt2

@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun f (Int) Int)
+(define-fun P ((x Int)) Bool (forall ((x Int)) (> (f x) 0)))
+(assert (P 0))
+(assert (= (f 0) 0))
+(check-sat)

test/regress/cli/regress0/proofs/var-eq-elim-tester-simple.smt2

@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatype List ((cons (head Int) (tail List)) (nil)))
+(declare-fun P (List List) Bool)
+(assert (forall ((y List) (x List)) (=> ((_ is cons) x) (P x y))))
+(assert (not (P (cons 0 nil) nil)))
+(check-sat)

test/regress/cli/regress0/quantifiers/dd_O512_prefix_sum_var_elim.smt2

@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const x9 Bool)
+(declare-const x Int)
+(declare-const x1 Int)
+(assert (exists ((a Int)) (and (exists ((s Int)) (and (exists ((a Int)) (and (forall ((o Bool)) (not (ite x9 (forall ((k Int)) true) (= o (= 0 (ite x9 x x1)))))))))))))
+(check-sat)

test/regress/cli/regress0/quantifiers/dd_rts-quant-elim-eq-tester.smt2

@@ -0,0 +1,10 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ((Formula!953 0)) (((And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32))))))
+(declare-fun error_value!964 () Bool)
+(declare-fun isNNF!208 (Formula!953) Bool)
+(declare-fun nnf!206 (Formula!953) Formula!953)
+(declare-fun error_value!966 () Formula!953)
+(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite ((_ is And!954) f!207) (and (isNNF!208 (rhs!956 f!207))) (ite ((_ is Or!959) f!207) (and (isNNF!208 (rhs!961 f!207))) (ite ((_ is Not!957) f!207) false (ite ((_ is Variable!962) f!207) true error_value!964)))))))
+(assert (exists ((formula!205 Formula!953)) (not (=> ((_ is Variable!962) formula!205) (isNNF!208 (ite ((_ is And!954) formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite ((_ is Or!959) formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and ((_ is Not!957) formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and ((_ is Not!957) formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and ((_ is Not!957) formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite ((_ is Not!957) formula!205) formula!205 (ite ((_ is Variable!962) formula!205) formula!205 error_value!966))))))))))))
+(check-sat)

test/regress/cli/regress0/seq/seq-unify-pf.smt2

@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; DISABLE-TESTER: cpc
+(set-logic ALL)
+(declare-fun x () Int)
+(declare-fun y () (Seq Int))
+(declare-fun z () (Seq Int))
+
+(assert (= (str.len y) (str.len z)))
+(assert (= (seq.++ (seq.unit 0) (seq.unit 1) y (seq.unit x) (seq.unit 0) (seq.unit 1) y)
+           (seq.++ (seq.unit 0) (seq.unit 1) z (seq.unit x) (seq.unit 1) (seq.unit 1) z))
+)
+(check-sat)

test/regress/cli/regress0/strings/ctn-repl-to-ctn.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (not (=
+(str.contains (str.replace x y x) y) (str.contains x y)
+)))
+(check-sat)

test/regress/cli/regress0/strings/ctn-split-no-overlap.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (str.contains (str.++ x "ABC" y) "DE"))
+(assert (not (str.contains x "DE")))
+(assert (not (str.contains y "DE")))
+(check-sat)

test/regress/cli/regress0/strings/dd_67_str_at_eval.smt2

@@ -0,0 +1,4 @@
+; EXPECT: unsat
+(set-logic ALL)
+(assert (>= (ite (str.prefixof "" (str.at "" 0)) 0 0) 1))
+(check-sat)

test/regress/cli/regress0/strings/dd_a1d_static_rewrite.smt2

@@ -0,0 +1,5 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun u () String)
+(assert (and (not (= 0 (ite (str.contains (str.substr u 0 1) "A") 1 0))) (not (= 0 (ite (= "" (str.replace (str.substr u 0 1) "A" "a")) 1 0)))))
+(check-sat)

test/regress/cli/regress0/strings/dd_a68_pp_static.smt2

@@ -0,0 +1,5 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun u () String)
+(assert (not (= 0 (ite (= "pr" (str.replace (str.substr u 0 1) "A" "")) 1 0))))
+(check-sat)

test/regress/cli/regress0/strings/dd_dd_norn_235_f_endpoint_eq.smt2

@@ -0,0 +1,5 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun v () String)
+(assert (str.in_re (str.++ v v) (re.++ (str.to_re "a") (re.union (str.to_re "") (re.++ (str.to_re "z") (re.union (str.to_re "") (str.to_re "a")))))))
+(check-sat)

test/regress/cli/regress0/strings/dd_slog_2087_ctn_split.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun _7 () String)
+(declare-fun x () String)
+(assert (= "" (str.++ _7 _7)))
+(assert (= (str.++ "{" _7) (str.++ x "")))
+(assert (str.in_re (str.++ x (str.++ x "")) (re.++ (re.* re.allchar) (re.++ (str.to_re "3c") (re.* re.allchar)))))
+(check-sat)

test/regress/cli/regress0/strings/prefix-suffix-eval.smt2

@@ -0,0 +1,14 @@
+; EXPECT: unsat
+(set-logic ALL)
+
+(assert (or
+
+(not (= (str.prefixof "AB" "ABC") true))
+(not (= (str.prefixof "ABC" "AB") false))
+(not (= (str.prefixof "ABC" "") false))
+(not (= (str.suffixof "BC" "ABC") true))
+(not (= (str.suffixof "ABC" "BC") false))
+(not (= (str.suffixof "ABC" "") false))
+
+))
+(check-sat)

test/regress/cli/regress0/strings/rw_508_suffixof.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () Int)
+(assert (not (= (str.suffixof "B" (str.replace "B" "A" x)) true)))
+(check-sat)
+(exit)

test/regress/cli/regress0/strings/rw_555.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () Int)
+(assert (not (= (= "" (str.replace "A" x y)) (= "A" (str.replace "" y x)))))
+(check-sat)
+(exit)

test/regress/cli/regress0/strings/small_pymongo_repl_char.smt2

@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun uri () String)
+(assert (not
+(= (str.contains (str.replace (str.substr (str.substr uri 10 (+ (- 10) (str.len uri))) 0 (+ 1 (str.indexof (str.substr uri 10 (+ (- 10) (str.len uri))) "+" 0))) "+" " ") "@") (or (str.contains (str.substr (str.substr uri 10 (+ (- 10) (str.len uri))) 0 (+ 1 (str.indexof (str.substr uri 10 (+ (- 10) (str.len uri))) "+" 0))) "@") (and (str.contains (str.substr (str.substr uri 10 (+ (- 10) (str.len uri))) 0 (+ 1 (str.indexof (str.substr uri 10 (+ (- 10) (str.len uri))) "+" 0))) "+") (str.contains " " "@"))))
+))
+(check-sat)

test/regress/cli/regress0/strings/str-repl-find-pre.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun purify_81 () String)
+(declare-fun purify_82 () String)
+(assert (not
+(= (str.replace (str.++ purify_81 "A" purify_82) "A" "a") (str.++ (str.replace (str.++ purify_81 "A") "A" "a") purify_82))
+))
+(check-sat)

test/regress/cli/regress0/strings/update-rewrites-simple.smt2

@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () String)
+(assert (or
+(not (= (str.update (str.++ "ABC" x) 1 "A") (str.++ "AAC" x)))
+(not (= (str.update "ABCE" 2 (str.++ "DDD" x)) "ABDD"))
+)
+)
+(check-sat)