projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ac8516) | patch
Improve error message when not using strings-exp (#8203)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Mar 2022 18:16:20 +0000 (12:16 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Mar 2022 18:16:20 +0000 (18:16 +0000)
commitd07ce1107a4431e4d3e584ae731fe19b51c19631
treea3345da1237bfd204b81a70eef5a9aa2acd99deatree
parent0ac85165d7550f5206593b0ea6440979050fa736commit | diff
Improve error message when not using strings-exp (#8203)

Fixes #6005.

Also improves smt2 printing of sequences so that we print the compliant kinds, which is work towards cvc5/cvc5-wishues#106.
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/issue6005-no-strings-exp.smt2 [new file with mode: 0644] blob