summaryrefslogtreecommitdiff
path: root/test/regress/regress0/print_model.cvc
diff options
context:
space:
mode:
authorYing Sheng <sqy1415@gmail.com>2020-03-07 21:01:16 -0800
committerGitHub <noreply@github.com>2020-03-07 21:01:16 -0800
commita0b35a8ba9c47ed521082c5ac5a8f50909d9f7c4 (patch)
tree78ac2d6fcc4f93145bfd199844e5aadf3c610847 /test/regress/regress0/print_model.cvc
parent76c1710e99f2e9ca2109762394eaefcbc4a5557c (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_model.cvc')
-rw-r--r--test/regress/regress0/print_model.cvc12
1 files changed, 12 insertions, 0 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback