diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4eeba4e9d..b42b9a699 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -550,6 +550,9 @@ class theory_lra::imp { return get_enode(n); } else { + if (reflect(n)) + for (expr* arg : *n) + th.ensure_enode(arg); return ctx().mk_enode(n, !reflect(n), false, enable_cgc_for(n)); } }