Skip to content

Commit c61140c

Browse files
hyperpolymathclaude
andcommitted
fix(exchange): smtlib split_paren_block takes &str not String
Two type-error sites at smtlib.rs:284 + :298 — split_first_token returns (String, String) and the second was being passed to split_paren_block which expects &str. Pass &after_name. Library now compiles clean: cargo check --lib finishes in ~24s across all saturation-campaign additions (corpus / verification / exchange). Lane: prover-corpus-saturation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 4a0b068 commit c61140c

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/rust/exchange/smtlib.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,7 @@ fn parse_command(expr: &str) -> Result<SmtLibCommand, ExchangeError> {
281281
"declare-fun" => {
282282
// (declare-fun NAME (P1 P2 ...) RET)
283283
let (name, after_name) = split_first_token(rest);
284-
let (params_block, ret) = split_paren_block(after_name)?;
284+
let (params_block, ret) = split_paren_block(&after_name)?;
285285
let params: Vec<String> = params_block
286286
.split_whitespace()
287287
.map(str::to_string)
@@ -295,7 +295,7 @@ fn parse_command(expr: &str) -> Result<SmtLibCommand, ExchangeError> {
295295
"define-fun" => {
296296
// (define-fun NAME ((x T) ...) RET BODY)
297297
let (name, after_name) = split_first_token(rest);
298-
let (params_block, after_params) = split_paren_block(after_name)?;
298+
let (params_block, after_params) = split_paren_block(&after_name)?;
299299
let params = parse_typed_params(&params_block);
300300
let (ret, body) = split_first_token(after_params.trim());
301301
SmtLibCommand::DefineFun {

0 commit comments

Comments
 (0)