summaryrefslogtreecommitdiff
path: root/test/regress/regress0/boolean-terms.cvc
AgeCommit message (Collapse)Author
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2012-11-27Functions and predicates over Boolean now work with --check-models and ↵Morgan Deters
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.)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback