Fix `(set-info <sexpr>)` parsing and printing bugs. (#7427)

Given
```smt2
(set-info :source (0 1 True False x ""))
```
`cvc5` currently prints the command below with `-o raw-benchmark`
```smt2
(set-info : |(0 1 True False x )|)
```
This PR ensures that `cvc5` correctly prints the command by
- Parsing and storing keywords eagerly before parsing their values.
- Removing pre-processing steps done to symbols and string literals.

4 files changed, 7 insertions, 6 deletions

diff --git a/test/regress/regress0/bug522.smt2 b/test/regress/regress0/bug522.smt2
index 3a9ea0eaa..ad6e526a8 100644
--- a/test/regress/regress0/bug522.smt2
+++ b/test/regress/regress0/bug522.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
 ; EXPECT: sat
-(set-option :incremental "true")
+(set-option :incremental true)
 (set-logic QF_UF)
 
 (push 1)
diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2
index 2a464571c..41012f888 100644
--- a/test/regress/regress0/options/ast-and-sexpr.smt2
+++ b/test/regress/regress0/options/ast-and-sexpr.smt2
@@ -13,5 +13,6 @@
 (get-option :command-verbosity)
 ; There is no SMT option to get the verbosity of a specific command
 
-(set-info :source (0 1 True False x ""))
+(set-info :source (true false (- 15) 15 15.0 #b00001111 #x0f x |x 
+"| "" """"))
 (get-info :status)
diff --git a/test/regress/regress1/quantifiers/bi-artm-s.smt2 b/test/regress/regress1/quantifiers/bi-artm-s.smt2
index af8ee945d..9c6b821b5 100644
--- a/test/regress/regress1/quantifiers/bi-artm-s.smt2
+++ b/test/regress/regress1/quantifiers/bi-artm-s.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --fmf-bound-lazy
 ; EXPECT: unsat
-(set-option :incremental "false")
+(set-option :incremental false)
 (set-info :status unsat)
 (set-logic ALL)
 (declare-fun Y () String)
diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
index c0b3aac7c..4a132a39b 100644
--- a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
+++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
-; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; COMMAND-LINE: -q --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: -q --full-saturate-quant --ee-mode=central
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
@@ -23,7 +23,7 @@
 (declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
 (assert (= 0 (|l#R| $EmptyValueArray)))
 (assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i))))))))
-(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid)))
+(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid || :skolemid ||)))
 (declare-fun |Select_[$Location]$bool| (b T@$Location) Bool)
 (declare-fun $m@@0 () T@M)
 (declare-fun $abort_flag@2 () Bool)