You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I am developing a project using Z3 as a theorem prover for checking properties. To this end I need to build a solver containing the main part of a theory and then check assertions constructed in runtime. To this end I start by building a solver from a file containing that initial theory:
Later, as I need to parse a string and build a new assertion, I invoke "Z3_parser_context_from_string (ctx, parserctx, buffer);" (by previously invoking "parserctx = Z3_mk_parser_context(ctx);"). The problem I am facing is that while both functions involving parsing under a parser_context are declared in the header, for some reason, the linker fails to find it in libz3.a.
I will be very grateful for any help you could provide.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
I am developing a project using Z3 as a theorem prover for checking properties. To this end I need to build a solver containing the main part of a theory and then check assertions constructed in runtime. To this end I start by building a solver from a file containing that initial theory:
...
Z3_solver_from_file(ctx, solver, filterDef);
Later, as I need to parse a string and build a new assertion, I invoke "Z3_parser_context_from_string (ctx, parserctx, buffer);" (by previously invoking "parserctx = Z3_mk_parser_context(ctx);"). The problem I am facing is that while both functions involving parsing under a parser_context are declared in the header, for some reason, the linker fails to find it in libz3.a.
I will be very grateful for any help you could provide.
Beta Was this translation helpful? Give feedback.
All reactions