diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-03-07 21:01:16 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-07 21:01:16 -0800 |
commit | a0b35a8ba9c47ed521082c5ac5a8f50909d9f7c4 (patch) | |
tree | 78ac2d6fcc4f93145bfd199844e5aadf3c610847 /test/regress/regress0/print_lambda.cvc | |
parent | 76c1710e99f2e9ca2109762394eaefcbc4a5557c (diff) |
Explicit end marker for models printed in the CVC language (#3934)
Fixes https://github.com/CVC4/cvc4-wishues/issues/9.
When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed.
This change adds begin and end markers as the example below:
```
MODEL BEGIN
x : INT = -3;
y : INT = 0;
z : INT = 0;
MODEL END;
```
Diffstat (limited to 'test/regress/regress0/print_lambda.cvc')
-rw-r--r-- | test/regress/regress0/print_lambda.cvc | 2 |
1 files changed, 2 insertions, 0 deletions
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; |