diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/print_lambda.cvc | 2 | ||||
| -rw-r--r-- | test/regress/regress0/print_model.cvc | 12 |
3 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5eaaf3e67..3bcbfa859 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -645,6 +645,7 @@ set(regress_0_tests regress0/preprocess/preprocess_14.cvc regress0/preprocess/preprocess_15.cvc regress0/print_lambda.cvc + regress0/print_model.cvc regress0/printer/bv_consts_bin.smt2 regress0/printer/bv_consts_dec.smt2 regress0/printer/empty_sort.smt2 diff --git a/test/regress/regress0/print_lambda.cvc b/test/regress/regress0/print_lambda.cvc index 548623954..99e5ff174 100644 --- a/test/regress/regress0/print_lambda.cvc +++ b/test/regress/regress0/print_lambda.cvc @@ -1,7 +1,9 @@ % SCRUBBER: sed -e 's/f : (INT) -> INT = (LAMBDA(.*:INT): 0);$/f : (INT) -> INT = (LAMBDA(VAR:INT): 0);/' % COMMAND-LINE: --produce-models % EXPECT: sat +% EXPECT: MODEL BEGIN % EXPECT: f : (INT) -> INT = (LAMBDA(VAR:INT): 0); +% EXPECT: MODEL END; f : INT -> INT; ASSERT f(1) = 0; diff --git a/test/regress/regress0/print_model.cvc b/test/regress/regress0/print_model.cvc new file mode 100644 index 000000000..0ad9ddf4c --- /dev/null +++ b/test/regress/regress0/print_model.cvc @@ -0,0 +1,12 @@ +% COMMAND-LINE: --produce-models +% EXPECT: sat +% EXPECT: MODEL BEGIN +% EXPECT: s1 : INT = 2; +% EXPECT: s2 : INT = 1; +% EXPECT: MODEL END; + +OPTION "produce-models"; +s1, s2 : INT; +ASSERT s1 = 2; +CHECKSAT s2 > 0 AND s2 < s1; +COUNTERMODEL; |