mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a990e7f02e
commit
31a6788859
|
@ -835,6 +835,8 @@ void tst_visit() {
|
||||||
std::cout << "visit example\n";
|
std::cout << "visit example\n";
|
||||||
context c;
|
context c;
|
||||||
|
|
||||||
|
// only one of the occurrences of x*x is visited
|
||||||
|
// because they are the same subterms
|
||||||
expr x = c.int_const("x");
|
expr x = c.int_const("x");
|
||||||
expr y = c.int_const("y");
|
expr y = c.int_const("y");
|
||||||
expr z = c.int_const("z");
|
expr z = c.int_const("z");
|
||||||
|
|
Loading…
Reference in a new issue