diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-04 22:26:40 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-04 22:26:40 +0000 |
commit | 3609fb41d7744b3a7d74e44f7bedc4d4c522c938 (patch) | |
tree | 011a3fa796fdb98bb3b9a1b425d12c678535f294 /test/regress/regress0/unconstrained | |
parent | 468c5bc5d8b63ec6818813270225e09383dd79ff (diff) |
Added preprocessing pass that propagates unconstrained values - solves all of
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed
Diffstat (limited to 'test/regress/regress0/unconstrained')
52 files changed, 1275 insertions, 0 deletions
diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am new file mode 100644 index 000000000..241b78848 --- /dev/null +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -0,0 +1,78 @@ +BINARY = cvc4 +if PROOF_REGRESSIONS +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY) +else +TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY) +endif + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + arith2.smt2 \ + arith3.smt2 \ + arith4.smt2 \ + arith5.smt2 \ + arith6.smt2 \ + arith7.smt2 \ + arith.smt2 \ + array1.smt2 \ + bvbool2.smt2 \ + bvbool3.smt2 \ + bvbool.smt2 \ + bvcmp.smt2 \ + bvconcat2.smt2 \ + bvconcat.smt2 \ + bvdiv2.smt2 \ + bvdiv.smt2 \ + bvext.smt2 \ + bvite.smt2 \ + bvmul2.smt2 \ + bvmul3.smt2 \ + bvmul.smt2 \ + bvnot.smt2 \ + bvsle2.smt2 \ + bvsle3.smt2 \ + bvsle4.smt2 \ + bvsle5.smt2 \ + bvsle.smt2 \ + bvslt2.smt2 \ + bvslt3.smt2 \ + bvslt4.smt2 \ + bvslt5.smt2 \ + bvslt.smt2 \ + bvule2.smt2 \ + bvule3.smt2 \ + bvule4.smt2 \ + bvule5.smt2 \ + bvule.smt2 \ + bvult2.smt2 \ + bvult3.smt2 \ + bvult4.smt2 \ + bvult5.smt2 \ + bvult.smt2 \ + geq.smt2 \ + gt.smt2 \ + leq.smt2 \ + lt.smt2 \ + uf1.smt2 \ + uf2.smt2 \ + xor.smt2 + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2 new file mode 100644 index 000000000..dc2b27414 --- /dev/null +++ b/test/regress/regress0/unconstrained/arith.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (< v2 100)) +(assert (not (= (a2 (- (+ v1 5) v2)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2 new file mode 100644 index 000000000..f9e829e45 --- /dev/null +++ b/test/regress/regress0/unconstrained/arith2.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFLIRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun v3 () Real) +(assert (= (+ v1 v2) v3)) +(assert (< v3 v2)) +(assert (> v3 (- v2 1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2 new file mode 100644 index 000000000..83634a50a --- /dev/null +++ b/test/regress/regress0/unconstrained/arith3.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFLIRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun v3 () Int) +(declare-fun v4 () Int) +(assert (= (* v1 v2) v3)) +(assert (< v3 v4)) +(assert (> v3 (- v4 1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2 new file mode 100644 index 000000000..8cb825a8d --- /dev/null +++ b/test/regress/regress0/unconstrained/arith4.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_AUFLIRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun v3 () Int) +(declare-fun v4 () Int) +(declare-fun v5 () Real) +(assert (= (* v1 v2) (+ (* v3 v4) v5))) +(assert (< v5 1)) +(assert (> v5 0)) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2 new file mode 100644 index 000000000..de1e305bc --- /dev/null +++ b/test/regress/regress0/unconstrained/arith5.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFBVLRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Real) +(declare-fun a2 (Real) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (* 2 v1)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2 new file mode 100644 index 000000000..05653415f --- /dev/null +++ b/test/regress/regress0/unconstrained/arith6.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFBVLRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Real) +(declare-fun a2 (Real) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (/ v1 2)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2 new file mode 100644 index 000000000..6cc063ca4 --- /dev/null +++ b/test/regress/regress0/unconstrained/arith7.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_AUFLIRA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v1 () Int) +(declare-fun v2 () Real) +(assert (= (/ v1 2) v2)) +(assert (< v2 (/ 1 2))) +(assert (> v2 0)) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2 new file mode 100644 index 000000000..82f084e87 --- /dev/null +++ b/test/regress/regress0/unconstrained/array1.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFBV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () (_ BitVec 16)) +(declare-fun a2 () (Array (_ BitVec 16) (_ BitVec 1024))) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (select a2 v1) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2 new file mode 100644 index 000000000..0dded2a2f --- /dev/null +++ b/test/regress/regress0/unconstrained/bvbool.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun p1 () Bool) +(declare-fun p2 () Bool) +(declare-fun p3 () Bool) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2 new file mode 100644 index 000000000..949096224 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvbool2.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun p1 () Bool) +(declare-fun p2 () Bool) +(declare-fun p3 () Bool) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (= (bvand x0 x1) ((_ extract 9 0) v3))) +(assert (= x1 (_ bv0 10))) +(assert (= v3 (_ bv1 1024))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2 new file mode 100644 index 000000000..6f72246f0 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvbool3.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun p1 () Bool) +(declare-fun p2 () Bool) +(declare-fun p3 () Bool) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (=> (or p1 p1) (and (= (bvnor (bvnand (bvor x1 x1) (bvand x0 x0)) x3) ((_ extract 9 0) v3)) p1)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvbool3.smt3 b/test/regress/regress0/unconstrained/bvbool3.smt3 new file mode 100644 index 000000000..7c9362672 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvbool3.smt3 @@ -0,0 +1,37 @@ +(set-logic QF_AUFBVLIA) +(set-info :source | +This benchmark demonstrates the need for propagating unconstrained arrays +and bit-vectors. + +Contributed by Robert Brummayer (robert.brummayer@gmail.com) +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun p1 () Bool) +(declare-fun p2 () Bool) +(declare-fun p3 () Bool) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2 new file mode 100644 index 000000000..ba7316324 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvcmp.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () (_ BitVec 1)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (= (bvcomp v1 (_ bv0 1)) ((_ extract 0 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2 new file mode 100644 index 000000000..e2941b34a --- /dev/null +++ b/test/regress/regress0/unconstrained/bvconcat.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (= (concat (bvlshr (bvashr (bvudiv x0 x1) (bvurem x2 x3)) (bvudiv x4 x5)) (bvurem x6 x7)) ((_ extract 19 0) v3)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2 new file mode 100644 index 000000000..aa901b9b0 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvconcat2.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun x8 () (_ BitVec 10)) +(declare-fun x9 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= (concat x0 x0) (_ bv1 20))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2 new file mode 100644 index 000000000..d3cadf6c8 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvdiv.smt2 @@ -0,0 +1,33 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun x8 () (_ BitVec 10)) +(declare-fun x9 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (= (bvshl (bvlshr (bvashr (bvudiv x0 x1) (bvurem x2 x3)) (bvudiv x4 x5)) (bvurem x6 x7)) ((_ extract 9 0) v4)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvdiv2.smt2 b/test/regress/regress0/unconstrained/bvdiv2.smt2 new file mode 100644 index 000000000..6314701b3 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvdiv2.smt2 @@ -0,0 +1,26 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun x8 () (_ BitVec 10)) +(declare-fun x9 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= (bvudiv x0 x0) (_ bv1 10)) + ) +) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2 new file mode 100644 index 000000000..56289e245 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvext.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (= ((_ extract 3 0) v1) ((_ extract 3 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2 new file mode 100644 index 000000000..9e1ecc193 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvite.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (= (ite (= x0 ((_ extract 9 0) v3)) ((_ extract 0 0) v4) (bvnot ((_ + extract 0 0) v4))) ((_ extract 0 0) v3)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2 new file mode 100644 index 000000000..fc56695f5 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvmul.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (= (bvmul x0 x1) ((_ extract 9 0) v3)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2 new file mode 100644 index 000000000..89e4ff569 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvmul2.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun x8 () (_ BitVec 10)) +(declare-fun x9 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= (bvmul x0 (_ bv2 10)) (_ bv1 10))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2 new file mode 100644 index 000000000..ea67a1b5a --- /dev/null +++ b/test/regress/regress0/unconstrained/bvmul3.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (= (bvmul x0 (_ bv15 10)) ((_ extract 9 0) v3)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2 new file mode 100644 index 000000000..22fc7e7d2 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvnot.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () (_ BitVec 1)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (= (bvnot (bvneg v1)) ((_ extract 0 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2 new file mode 100644 index 000000000..702f9d7a0 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvsle.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (bvsle x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2 new file mode 100644 index 000000000..b797fa4e8 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvsle2.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x0 (_ bv513 10))) +(assert + (not + (= + (a2 + (ite + (bvsle x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2 new file mode 100644 index 000000000..4d897830c --- /dev/null +++ b/test/regress/regress0/unconstrained/bvsle3.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvslt x0 (_ bv513 10))) +(assert (not (bvsle x0 x1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2 new file mode 100644 index 000000000..8927a5f2e --- /dev/null +++ b/test/regress/regress0/unconstrained/bvsle4.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x1 (_ bv510 10))) +(assert + (not + (= + (a2 + (ite + (bvsle x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2 new file mode 100644 index 000000000..1aceacbe3 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvsle5.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvsgt x1 (_ bv510 10))) +(assert (not (bvsle x0 x1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2 new file mode 100644 index 000000000..f98375653 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvslt.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (bvslt x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2 new file mode 100644 index 000000000..e56500ad2 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvslt2.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x0 (_ bv510 10))) +(assert + (not + (= + (a2 + (ite + (bvslt x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2 new file mode 100644 index 000000000..a4af152f1 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvslt3.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvsgt x0 (_ bv510 10))) +(assert (bvslt x0 x1)) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2 new file mode 100644 index 000000000..d702b6d1a --- /dev/null +++ b/test/regress/regress0/unconstrained/bvslt4.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x1 (_ bv513 10))) +(assert + (not + (= + (a2 + (ite + (bvslt x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2 new file mode 100644 index 000000000..f4b6a7a63 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvslt5.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvslt x1 (_ bv513 10))) +(assert (bvslt x0 x1)) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2 new file mode 100644 index 000000000..cbbb4cc6e --- /dev/null +++ b/test/regress/regress0/unconstrained/bvule.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (bvule x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2 new file mode 100644 index 000000000..0e6f5916b --- /dev/null +++ b/test/regress/regress0/unconstrained/bvule2.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x0 (_ bv1 10))) +(assert + (not + (= + (a2 + (ite + (bvule x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2 new file mode 100644 index 000000000..11e3a9877 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvule3.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvult x0 (_ bv1 10))) +(assert (not (bvule x0 x1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2 new file mode 100644 index 000000000..b8d978b71 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvule4.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x1 (_ bv1022 10))) +(assert + (not + (= + (a2 + (ite + (bvule x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2 new file mode 100644 index 000000000..cd927d0c6 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvule5.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvugt x1 (_ bv1022 10))) +(assert (not (bvule x0 x1))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2 new file mode 100644 index 000000000..fb94994b4 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvult.smt2 @@ -0,0 +1,31 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (bvult x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2 new file mode 100644 index 000000000..3fb4a0d23 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvult2.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x0 (_ bv1022 10))) +(assert + (not + (= + (a2 + (ite + (bvult x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2 new file mode 100644 index 000000000..b11ab9da3 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvult3.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvugt x0 (_ bv1022 10))) +(assert (bvult x0 x1)) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2 new file mode 100644 index 000000000..8170ec280 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvult4.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= x1 (_ bv1 10))) +(assert + (not + (= + (a2 + (ite + (bvult x0 x1) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2 new file mode 100644 index 000000000..545bcbf64 --- /dev/null +++ b/test/regress/regress0/unconstrained/bvult5.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (bvult x1 (_ bv1 10))) +(assert (bvult x0 x1)) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/files b/test/regress/regress0/unconstrained/files new file mode 100644 index 000000000..8a0f48889 --- /dev/null +++ b/test/regress/regress0/unconstrained/files @@ -0,0 +1,49 @@ +arith2.smt2 +arith3.smt2 +arith4.smt2 +arith5.smt2 +arith6.smt2 +arith7.smt2 +arith.smt2 +array1.smt2 +bvbool2.smt2 +bvbool3.smt2 +bvbool.smt2 +bvcmp.smt2 +bvconcat2.smt2 +bvconcat.smt2 +bvdiv2.smt2 +bvdiv.smt2 +bvext.smt2 +bvite.smt2 +bvmul2.smt2 +bvmul3.smt2 +bvmul.smt2 +bvnot.smt2 +bvsle2.smt2 +bvsle3.smt2 +bvsle4.smt2 +bvsle5.smt2 +bvsle.smt2 +bvslt2.smt2 +bvslt3.smt2 +bvslt4.smt2 +bvslt5.smt2 +bvslt.smt2 +bvule2.smt2 +bvule3.smt2 +bvule4.smt2 +bvule5.smt2 +bvule.smt2 +bvult2.smt2 +bvult3.smt2 +bvult4.smt2 +bvult5.smt2 +bvult.smt2 +geq.smt2 +gt.smt2 +leq.smt2 +lt.smt2 +uf1.smt2 +uf2.smt2 +xor.smt2 diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2 new file mode 100644 index 000000000..818bb55b3 --- /dev/null +++ b/test/regress/regress0/unconstrained/geq.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (>= v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2 new file mode 100644 index 000000000..76b119e42 --- /dev/null +++ b/test/regress/regress0/unconstrained/gt.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (> v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2 new file mode 100644 index 000000000..6c03fc254 --- /dev/null +++ b/test/regress/regress0/unconstrained/leq.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (<= v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2 new file mode 100644 index 000000000..637a6407f --- /dev/null +++ b/test/regress/regress0/unconstrained/lt.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Int) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (ite (< v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2 new file mode 100644 index 000000000..0b2a95f49 --- /dev/null +++ b/test/regress/regress0/unconstrained/uf1.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun v1 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (not (= (a2 (- v1)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/uf2.smt2 b/test/regress/regress0/unconstrained/uf2.smt2 new file mode 100644 index 000000000..0aa1617eb --- /dev/null +++ b/test/regress/regress0/unconstrained/uf2.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v1 () (_ BitVec 1)) +(declare-fun a2 ((_ BitVec 1)) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert (= (a2 (_ bv0 1)) v3)) +(assert (= (a2 (_ bv1 1)) v3)) +(assert (not (= (a2 v1) v3))) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2 new file mode 100644 index 000000000..4089bb5dc --- /dev/null +++ b/test/regress/regress0/unconstrained/xor.smt2 @@ -0,0 +1,33 @@ +(set-logic QF_AUFBVLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x0 () (_ BitVec 10)) +(declare-fun x1 () (_ BitVec 10)) +(declare-fun x2 () (_ BitVec 10)) +(declare-fun x3 () (_ BitVec 10)) +(declare-fun x4 () (_ BitVec 10)) +(declare-fun x5 () (_ BitVec 10)) +(declare-fun x6 () (_ BitVec 10)) +(declare-fun x7 () (_ BitVec 10)) +(declare-fun v2 () Int) +(declare-fun a2 (Int) (_ BitVec 1024)) +(declare-fun v3 () (_ BitVec 1024)) +(declare-fun v4 () (_ BitVec 1024)) +(declare-fun v5 () (_ BitVec 1024)) +(assert + (not + (= + (a2 + (ite + (= (xor (= (bvxor (bvxnor (bvadd (bvsub x0 ((_ extract 9 0) v3)) ((_ extract + 9 0) v4)) ((_ extract 9 0) v5)) ((_ extract 19 10) v3)) ((_ extract 19 10) + v4)) (= v3 v4)) (= v4 v5)) + v2 + 6) + ) + (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5)))) + ) + ) +(check-sat) +(exit) |