`Solver::get_model` fails to parse z3 output

[slerpyyy]

Hey, I tried to solve some equations with z3 through this library and ran into problems extracting the model for the found solution.

I ran the Solver::get_model function and z3 replied as follows to the (get-model) command:

(
  (define-fun x1 () Real
    (/ 1.0 4.0))
  (define-fun x0 () Real
    (/ 1.0 2.0))
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    (ite (and (= x!0 1.0) (= x!1 (- (/ 3.0 4.0)))) (- (/ 4.0 3.0))
    (ite (and (= x!0 1.0) (= x!1 (/ 3.0 4.0))) (/ 4.0 3.0)
      0.0)))
)

Yet, the function returned the following error:

Error(
    ParseError(
        "expected `)`",
        "=",
    ),
    State {
        next_error: None,
        backtrace: InternalBacktrace {
            backtrace: None,
        },
    },
)

To find the problem, I made a model parser that simply prints out the arguments it was called with. That gave me the following log:

input: "(/ 1.0 4.0)"
ident: "x1"
params: []
typ: "Real"

input: "(/ 1.0 2.0)"
ident: "x0"
params: []
typ: "Real"

input: "(ite (and (" # <-- broken
ident: "/0"
params: [("x!0", "Real"), ("x!1", "Real")]
typ: "Real"

I believe this is a problem with SmtParser::try_load_sexpr but I might be wrong.

[slerpyyy]

Append this to the end of rsmt2/src/parse.rs for a failing unit test:

#[cfg(test)]
mod test {
    use super::*;

    #[test]
    fn parse_model_tricky() {
        let input = "(
  (define-fun x1 () Real
      (/ 1.0 4.0))
  (define-fun x0 () Real
      (/ 1.0 2.0))
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
      (ite (and (= x!0 1.0) (= x!1 (- (/ 3.0 4.0)))) (- (/ 4.0 3.0))
      (ite (and (= x!0 1.0) (= x!1 (/ 3.0 4.0))) (/ 4.0 3.0)
      0.0)))
)";

        let mut parser = SmtParser::new(input.as_bytes());
        parser.get_model(false, ()).unwrap();
    }
}

[AdrienChampion]

Thank you for opening this issue 🐱

You're right, there seems to be a (dumb) bug in try_load_sexpr. I haven't touched this code in a while, so I fixed the problem you have but it made others appear.

I need to find some time to take care of this, it should be done next week.

[AdrienChampion]

I actually managed to fix pretty much everything, but now I have unrelated tests that fail because of what seems to be a problem in z3:

• https://github.com/Z3Prover/z3/issues/6273

As soon as I understand what's going on and confirm everything works fine I'll push a new rsmt2 version.

[AdrienChampion]

@slerpyyy alright I just merged and published a new version of rsmt2 with fixes for your issue and others.

Can you confirm that the problem is gone for rsmt2 v0.16.1?

If that's not the case, do reopen this issue 🐱

[AdrienChampion]

Also, thank you again for reporting this problem. My guess is that others have run into bugs such as these but did not report them.

I am very grateful that you took the time to help improve rsmt2! ❤️

[slerpyyy]

Yes, I have pulled your latest commits and it now parses the output correctly!

Thank you so much for fixing this quickly!