diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/bi-artm-s.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/bi-artm-s.smt2 | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/bi-artm-s.smt2 b/test/regress/regress1/quantifiers/bi-artm-s.smt2 new file mode 100644 index 000000000..b97c339fc --- /dev/null +++ b/test/regress/regress1/quantifiers/bi-artm-s.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --fmf-bound-lazy +; EXPECT: unsat +(set-option :incremental "false") +(set-info :status unsat) +(set-logic ALL_SUPPORTED) +(declare-fun Y () String) +(set-info :notes "ufP_1 is uf type conv P") +(declare-fun ufP_1 (Int) Int) +(set-info :notes "ufM_2 is uf type conv M") +(declare-fun ufM_2 (Int) Int) +(declare-fun z1_3 () String) +(declare-fun z2_4 () String) +(declare-fun z3_5 () String) +(declare-fun V_253 () String) +(declare-fun V_254 () String) + +(assert (or (= Y "1") (= Y "0"))) +(assert (>= (ufP_1 0) 32)) +(assert + +(forall ((V_243 Int)) +(or +(not (and (>= V_243 0) (>= (+ (str.len Y) (* (- 1) V_243)) 1))) +(and +(or (not (= (str.len Y) (+ 1 V_243))) (= (ufP_1 V_243) (ufM_2 V_243))) +(not (>= (ufM_2 V_243) 10)) +(not (or (not (= (str.len Y) (+ 1 V_243 (str.len V_253)))) (not (= Y (str.++ V_253 (ite (= (ufM_2 V_243) 0) "0" "1") V_254)))) ))) )) + +(check-sat) |