Allow unquoted symbols in new SMT backend output if they observe the `simple_symbols` definition.#6745

Closed

NlightNFotis wants to merge 9 commits intodiffblue:developfrom

NlightNFotis:escape_symbols_smt

Commits on Mar 30, 2022

Do not quote identifiers matching definition of simple_symbol from SMT-lib spec
NlightNFotis
committed
Change regex_match to match against the identifier rather than the converted string
NlightNFotis
committed
Change tests to reflect new reality around quoting symbols.
NlightNFotis
committed
Change regression testing suite to support building with cvc4 as well as z3
NlightNFotis
committed
Fix tests to admit unquoted symbols and change solver to cvc5 for CI compatibility.
NlightNFotis
committed
Optimise check for simple symbols

thomasspriggs
authored and
NlightNFotis
committed
Change `Makefile` in `regression/cbmc-incr-smt2` to support testing with multiple solvers.
NlightNFotis
committed

Commits on Mar 31, 2022