diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ce1cd1fbd..05faf040e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1031,7 +1031,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] | str[s,false] { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl; - sgt.d_expr = MK_CONST( ::CVC4::String(s) ); + sgt.d_expr = MK_CONST( ::CVC4::String(s, true) ); sgt.d_name = s; sgt.d_gterm_type = SygusGTerm::gterm_op; } @@ -2328,7 +2328,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_CONST( BitVector(binString, 2) ); } | str[s,false] - { expr = MK_CONST( ::CVC4::String(s) ); } + { expr = MK_CONST( ::CVC4::String(s, true) ); } | FP_RNE_TOK { expr = MK_CONST(roundNearestTiesToEven); } | FP_RNA_TOK { expr = MK_CONST(roundNearestTiesToAway); } | FP_RTP_TOK { expr = MK_CONST(roundTowardPositive); } |