diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-15 21:31:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-15 23:31:10 -0500 |
commit | e61c6ecf2e8c569d9f1b5f27ec1309371cc45cff (patch) | |
tree | 339ec96158b78b7e998a6c4edd16a4127a7fe8aa /test/regress/regress0 | |
parent | 85a3056bed70e226d9e17a1f5785d957628f9e26 (diff) |
bv2int: support models in tests (#5068)
Previous changes in this preprocessing pass have already enabled model generation when using it.
However, the satisfiable tests still had --no-check-models.
The changes in this PR:
All --no-check-models from current tests for the preprocessing pass are removed.
Refactoring of the relevant part of the code.
Solves CVC4/cvc4-projects#128.
Remark: disabling white-spaces when reviewing this PR is recommended.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/bv/bv_to_int1.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int2.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bitwise.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvmul1.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvmul2.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_elim_err.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_zext.smt2 | 2 |
9 files changed, 18 insertions, 17 deletions
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index f812ccbc8..970a9fd75 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2 index 00fd51baf..d60f4903b 100644 --- a/test/regress/regress0/bv/bv_to_int2.smt2 +++ b/test/regress/regress0/bv/bv_to_int2.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 index 6f08c2e8d..444551776 100644 --- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 index ec4206812..e21415244 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 @@ -1,10 +1,11 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) (declare-fun b () (_ BitVec 8)) (assert (bvult (bvmul a b) (bvudiv a b))) +(assert (bvugt a (_ bv0 8))) (check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index 4e940b5df..4bbe5685e 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 index c621aa112..5879542eb 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 index 8fbe96eab..f43c8c860 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (declare-sort S 0) diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 index b17aeeacf..01ee5dad8 100644 --- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_183_ () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index ab09d7341..42e06a940 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) |