Make CnfStream::toCNF iterative (#6757)

This commit makes toCNF() iterative to avoid this issue.
Note that the order in which nodes are visited and thus SatLiterals are
created remains the same.

Fixes #6111

2 files changed, 59 insertions, 0 deletions

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index e9fd47261..4811cca1b 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -51,6 +51,7 @@ cvc5_add_api_test(smt2_compliance)
 cvc5_add_api_test(two_solvers)
 cvc5_add_api_test(issue5074)
 cvc5_add_api_test(issue4889)
+cvc5_add_api_test(issue6111)
 
 # if we've built using libedit, then we want the interactive shell tests
 if (USE_EDITLINE)
diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp
new file mode 100644
index 000000000..bd7be2ad0
--- /dev/null
+++ b/test/api/issue6111.cpp
@@ -0,0 +1,58 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for issue #6111
+ *
+ */
+#include <iostream>
+#include <vector>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+int main()
+{
+  Solver solver;
+  solver.setLogic("QF_BV");
+  Sort bvsort12979 = solver.mkBitVectorSort(12979);
+  Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1");
+  Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10);
+
+  vector<Term> args1;
+  args1.push_back(zero);
+  args1.push_back(input2_1);
+  Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1);
+  solver.assertFormula(bvult_res);
+
+  Sort bvsort4 = solver.mkBitVectorSort(4);
+  Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42");
+  Sort bvsort8 = solver.mkBitVectorSort(8);
+  Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43");
+
+  vector<Term> args2;
+  args2.push_back(concat_result_42);
+  args2.push_back(
+      solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43}));
+  solver.assertFormula(solver.mkTerm(EQUAL, args2));
+
+  vector<Term> args3;
+  args3.push_back(concat_result_42);
+  args3.push_back(
+      solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43}));
+  solver.assertFormula(solver.mkTerm(EQUAL, args3));
+
+  cout << solver.checkSat() << endl;
+
+  return 0;
+}