Panic when parsing quoted identifiers

[rachitnigam]

SMTLIB allows for defining identifiers with restricted characters by wrapping them in |: |foo::bar@10|. However, the crate fails to parse such identifiers:

use easy_smt::{ContextBuilder, Response};

fn main() -> std::io::Result<()> {
    // Create a new context, backed by a Z3 subprocess.
    let mut ctx = ContextBuilder::new()
        .solver("z3", ["-smt2", "-in"])
        .replay_file(Some(std::fs::File::create("replay.smt2")?))
        .build()?;

    // Declare `x` and `y` variables that are bitvectors of width 32.
    let x = ctx.declare_const("|x::10|", ctx.int_sort())?;

    // Assert that `x * y = 18`.
    ctx.assert(ctx.eq(x, ctx.numeral(10)))?;

    // Check whether the assertions are satisfiable. They should be in this example.
    assert_eq!(ctx.check()?, Response::Sat);

    // Print the solution!
    let solution = ctx.get_value(vec![x])?;
    for (variable, value) in solution {
        println!("{} = {}", ctx.display(variable), ctx.display(value));
    }

    Ok(())
}

The expected output would be printing:

|x::10| = <value>

Unfortunately, we get:

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `2`,
 right: `5`', /Users/rachitnigam/.cargo/registry/src/index.crates.io-6f17d22bba15001f/easy-smt-0.2.0/src/context.rs:444:29
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Running the replay.smt2 file, we get the right answer:

% z3 -smt2 replay.smt2 
success
success
success
success
sat
((|x::10| 10))

It looks like we hit an assert! in implementation of get_value which is probably triggered because the parser doesn't handle quoted identifiers correctly.

[rachitnigam]

Digging a little deeper, the term x::10 is parsed as (quotes added to disambiguate):

( "|x" ":" ":10" "|" )