MCPcopy Create free account
hub / github.com/Z3Prover/z3 / parserExample5

Method parserExample5

examples/java/JavaGenericExample.java:1285–1302  ·  view source on GitHub ↗
(Context ctx)

Source from the content-addressed store, hash-verified

1283
1284 // / <remarks></remarks>
1285 public void parserExample5(Context ctx)
1286 {
1287 System.out.println("ParserExample5");
1288
1289 try
1290 {
1291 ctx.parseSMTLIB2String(
1292 /*
1293 * the following string has a parsing error: missing
1294 * parenthesis
1295 */
1296 "(declare-const x Int (declare-const y Int)) (assert (> x y))",
1297 null, null, null, null);
1298 } catch (Z3Exception e)
1299 {
1300 System.out.printf("Z3 error: %s%n", e);
1301 }
1302 }
1303
1304 // / Create an ite-Expr (if-then-else Exprs).
1305

Callers 1

mainMethod · 0.95

Calls 1

parseSMTLIB2StringMethod · 0.80

Tested by

no test coverage detected