From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 19 Jul 2017 19:59:36 +0000 (-0400)
Subject: Fix simple_vc_compat_cxx example (#202)
X-Git-Tag: cvc5-1.0.0~5713
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7fd11d0df4c257a916e93c3f44238f1d3f70f721;p=cvc5.git

Fix simple_vc_compat_cxx example (#202)

The CVC3 compatibility layer was broken because it was setting
simplification mode to SIMPLIFICATION_MODE_INCREMENTAL, which
is not supported anymore since commit
2dbe1f150d30f0fb0c8522f891104270ce09db4c . This commit changes
the compatibility layer to not set the option anymore.

This addresses bug 833, which had been reported on the cvc-bugs mailing list.
---

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 2757e3dbe..3309ce442 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -924,13 +924,16 @@ void CLFlags::setFlag(const std::string& name,
 }
 
 void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflags) {
+  // Note: SIMPLIFICATION_MODE_INCREMENTAL, which was used
+  // for CVC3 compatibility, is not supported by CVC4
+  // anymore.
+
   // always incremental and model-producing in CVC3 compatibility mode
   // also incrementally-simplifying and interactive
   d_smt->setOption("incremental", string("true"));
   // disable this option by default for now, because datatype models
   // are broken [MGD 10/4/2012]
   //d_smt->setOption("produce-models", string("true"));
-  d_smt->setOption("simplification-mode", string("incremental"));
   d_smt->setOption("interactive-mode", string("true"));// support SmtEngine::getAssertions()
 
   d_smt->setOption("statistics", string(clflags["stats"].getBool() ? "true" : "false"));