From 31a6788859d4fc05d2b88080d58014c328aa7262 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Oct 2019 12:39:57 -0700 Subject: [PATCH] comment Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 20bc89a46..cc1c4398a 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -835,6 +835,8 @@ void tst_visit() { std::cout << "visit example\n"; 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 y = c.int_const("y"); expr z = c.int_const("z");