Formalize more string skolems (#7554)

This properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules.

Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.

5 files changed, 61 insertions, 0 deletions

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index f6c1cf8df..56adf73e7 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -53,6 +53,7 @@ cvc5_add_api_test(issue5074)
 cvc5_add_api_test(issue4889)
 cvc5_add_api_test(issue6111)
 cvc5_add_api_test(proj-issue306)
+cvc5_add_api_test(proj-issue334)
 
 # if we've built using libedit, then we want the interactive shell tests
 if (USE_EDITLINE)
diff --git a/test/api/proj-issue306.cpp b/test/api/proj-issue306.cpp
index 664536a0b..35ecda567 100644
--- a/test/api/proj-issue306.cpp
+++ b/test/api/proj-issue306.cpp
@@ -1,3 +1,19 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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 project issue #306
+ *
+ */
+
 #include "api/cpp/cvc5.h"
 
 using namespace cvc5::api;
diff --git a/test/api/proj-issue334.cpp b/test/api/proj-issue334.cpp
new file mode 100644
index 000000000..bbb7f1a46
--- /dev/null
+++ b/test/api/proj-issue334.cpp
@@ -0,0 +1,36 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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 project issue #334
+ *
+ */
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  slv.setOption("produce-unsat-cores", "true");
+  Sort s1 = slv.mkBitVectorSort(1);
+  Sort s2 = slv.mkFloatingPointSort(8, 24);
+  Term val = slv.mkBitVector(32, "10000000110010111010111011000101", 2);
+  Term t1 = slv.mkFloatingPoint(8, 24, val);
+  Term t2 = slv.mkConst(s1);
+  Term t4 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, t2);
+  Term t5 = slv.mkTerm(Kind::STRING_FROM_CODE, t4);
+  Term t6 = slv.simplify(t5);
+  Term t7 = slv.mkTerm(Kind::STRING_LEQ, t5, t6);
+  slv.assertFormula(t7);
+  slv.simplify(t1);
+}
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7839dc7f2..da7c40bc2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2321,6 +2321,7 @@ set(regress_1_tests
   regress1/strings/policy_variable.smt2
   regress1/strings/pre_ctn_no_skolem_share.smt2
   regress1/strings/proj254-re-elim-agg.smt2
+  regress1/strings/proj-issue331.smt2
   regress1/strings/query4674.smt2
   regress1/strings/query8485.smt2
   regress1/strings/re-all-char-hard.smt2
diff --git a/test/regress/regress1/strings/proj-issue331.smt2 b/test/regress/regress1/strings/proj-issue331.smt2
new file mode 100644
index 000000000..e993419f1
--- /dev/null
+++ b/test/regress/regress1/strings/proj-issue331.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :check-proofs true)
+(set-info :status unsat)
+(declare-const x Int)
+(check-sat-assuming ((str.< (str.++ (str.from_int x) (str.replace_re (str.from_int x) re.none (str.from_int 0)) (str.replace_re (str.from_int x) re.none (str.from_int 0))) (str.from_int x))))