diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 22:40:05 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 22:40:05 +0000 |
| commit | 16d8379a9a87fe692c6f95a11300b43e4d2cba30 (patch) | |
| tree | 7a97c484de035ff6268d2fc572a418cd8d48faca /test | |
| parent | 551d1d37fe9c8ec25ddeac1e37b68d39158378ea (diff) | |
Functions and predicates over Boolean now work with --check-models and output correct
models for such functions (though they are somewhat ugly at present).
There's still a problem with model extraction, but it's not Boolean terms' fault.
Sometimes checkModel() can report that the model is just fine, but if a user extracts
values with getValue(), they find problems with the model (i.e., it doesn't satisfy some
assertions). This appears to be due to an asymmetry between how checkModel() works and
how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking
some more on it.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/boolean-terms.cvc | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 6af6fbf70..ffc9a4204 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -59,6 +59,7 @@ SMT2_TESTS = \ CVC_TESTS = \ boolean.cvc \ boolean-prec.cvc \ + boolean-terms.cvc \ hole6.cvc \ ite.cvc \ let.cvc \ diff --git a/test/regress/regress0/boolean-terms.cvc b/test/regress/regress0/boolean-terms.cvc new file mode 100644 index 000000000..5458f6c63 --- /dev/null +++ b/test/regress/regress0/boolean-terms.cvc @@ -0,0 +1,16 @@ +% EXPECT: sat +% EXIT: 10 +%OPTION "produce-models"; + +f : BOOLEAN -> INT; +x : INT; +p : BOOLEAN -> BOOLEAN; + +ASSERT f(p(TRUE)) = x; +ASSERT f(p(FALSE)) = x + 1; + +CHECKSAT; +%GET_VALUE f(p(TRUE)); +%GET_VALUE f(p(TRUE)) = x; +%GET_VALUE f(p(FALSE)) = x + 1; +%COUNTERMODEL; |