Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use the new version z3 #302

Open
Moorvan opened this issue Aug 3, 2022 · 0 comments
Open

Use the new version z3 #302

Moorvan opened this issue Aug 3, 2022 · 0 comments

Comments

@Moorvan
Copy link
Contributor

Moorvan commented Aug 3, 2022

In the current version of z3 in use, a problem is encountered with "Overflow encountered when expanding vector" during solving, which can be seen: Z3Prover/z3#864

It seems fixed in new version of z3. However, when I changed to use the new version of z3 in smt-switch, I meet:

Undefined symbols for architecture arm64:
  "mk_implies(probe*, probe*)", referenced from:
      sexpr2probe(cmd_context&, sexpr*) in libsmt-switch-z3.a(tactic_cmds.o)
  "fatal_error(int)", referenced from:
      datalog::check_table::empty() const in libsmt-switch-z3.a(dl_check_table.o)
  "mk_size_probe()", referenced from:
      install_tactics(tactic_manager&) in libsmt-switch-z3.a(install_tactic.o)
  "mk_const_probe(double)", referenced from:
      sexpr2probe(cmd_context&, sexpr*) in libsmt-switch-z3.a(tactic_cmds.o)
      mk_auflia_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(quant_tactics.o)
      mk_qfbv_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(qfbv_tactic.o)
      mk_qfidl_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(qfidl_tactic.o)
      mk_qflia_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(qflia_tactic.o)
 .....

It seems that api does not match.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant