diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 9853181ca..092ac022a 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -109,10 +109,12 @@ void tst_polynorm() { reg_decl_plugins(m); expr_ref fml(m); - fml = parse_fml(m, example2); - + fml = parse_fml(m, example1); std::cout << mk_pp(fml, m) << "\n"; + nf(fml); + fml = parse_fml(m, example2); + std::cout << mk_pp(fml, m) << "\n"; nf(fml);