Fix SMT-LIB conformance of echo and :error-behavior (#415, #416) - #652
Merged
Conversation
- echo now prints the string literal back with its surrounding double quotes, re-escaping embedded quotes to match how the lexer reads strings in the active SMT-LIB version (#416). - report :error-behavior as continued-execution, which is what Yices actually does: it reports an error and keeps executing commands rather than exiting (#415). - add regression tests iss415/iss416 and update the gold files of existing echo tests to the now-quoted output.
This was
linked to
issues
Jul 6, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes two SMT-LIB 2.6 conformance bugs in the
yices_smt2frontend.#416 —
echoomitted the surrounding double-quotesThe standard (§4.2.9): "(echo s) … simply prints back s as is—including the surrounding double-quotes." Yices printed only the decoded contents.
smt2_echonow reconstructs a valid string literal: it re-adds the surrounding quotes and re-escapes embedded quotes the same way the lexer reads them — doubling ("") in 2.5/2.6 mode, backslash (\",\\) in legacy 2.0 mode (§3.1).#415 —
:error-behaviormisreportedget-info :error-behaviorreturnedimmediate-exit, but Yices does not exit on command errors — it reports the error and keeps executing. Report the accurate valuecontinued-execution(§4.1.8).Confirmed against the SMT-LIB 2.6 standard
Verified verbatim against the SMT-LIB 2.6 reference (r2021-05-12):
(echo "ok")yields"ok", notok.\"can itself occur within a string literal only if duplicated … treat the sequence\"\"as an escape sequence." → the only escape is""; backslash is not special. This is why embedded quotes are doubled when re-emitting in 2.6 mode.immediate-exitorcontinued-execution. …continued-executionindicates that when an error is encountered, the solver will return to the state it was in immediately before the command triggering the error, and continue accepting and executing new commands." → matches Yices's actual behavior.Tests
iss415andiss416(the latter covers plain quoting, legacy\"escaping, and 2.6""doubling).test_qfaufbvlia,test_qfufbvlia,test_qfbvlra,mcsat/test_qfaufbvnia) to the now-quoted output. These gold files recorded the pre-fix (non-conformant) unquoted output; §4.2.9 mandates the quoted form.Follow-up
""string escape not supported by default. Per §3.1 the""escape is the only way to embed a quote in a 2.6 string literal, but Yices only accepts it when(set-info :smt-lib-version 2.5|2.6)is set (it flips the lexer'stwo_dot_five_variant); by default it still uses the legacy 2.0\"/\\escapes. Resolving "" escape sequence not supported in strings #417 means either making the 2.6""variant the default or adding a CLI flag to select it. Left out of this PR because it changes default lexer behavior and warrants a separate decision. This PR'ssmt2_echoalready re-escapes correctly under both variants, so it composes cleanly with whichever direction "" escape sequence not supported in strings #417 takes.