From 51721c308032fe67b7cd3dc391b3743ccb25e2ed Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 13 Jul 2020 20:56:12 +0200
Subject: [PATCH] Double SAT run for cex

---
 libsmtutil/Z3CHCInterface.cpp | 55 +++++++++++++++++++++++++++--------
 libsmtutil/Z3CHCInterface.h   |  3 ++
 libsolidity/formal/CHC.cpp    | 18 ++++++++++++
 3 files changed, 64 insertions(+), 12 deletions(-)

diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp
index 6381aaa54..4baf3bd0a 100644
--- a/libsmtutil/Z3CHCInterface.cpp
+++ b/libsmtutil/Z3CHCInterface.cpp
@@ -36,18 +36,7 @@ Z3CHCInterface::Z3CHCInterface():
 	z3::set_param("rewriter.pull_cheap_ite", true);
 	z3::set_param("rlimit", Z3Interface::resourceLimit);
 
-	// Spacer options.
-	// These needs to be set in the solver.
-	// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
-	z3::params p(*m_context);
-	// These are useful for solving problems with arrays and loops.
-	// Use quantified lemma generalizer.
-	p.set("fp.spacer.q3.use_qgen", true);
-	p.set("fp.spacer.mbqi", false);
-	// Ground pobs by using values from a model.
-	p.set("fp.spacer.ground_pobs", false);
-
-	m_solver.set(p);
+	enablePreProcessing();
 }
 
 void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
@@ -115,6 +104,48 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 	return {result, cex};
 }
 
+void Z3CHCInterface::enablePreProcessing()
+{
+	// Spacer options.
+	// These needs to be set in the solver.
+	// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
+	z3::params p(*m_context);
+	// These are useful for solving problems with arrays and loops.
+	// Use quantified lemma generalizer.
+	p.set("fp.spacer.q3.use_qgen", true);
+	p.set("fp.spacer.mbqi", false);
+	// Ground pobs by using values from a model.
+	p.set("fp.spacer.ground_pobs", false);
+
+	// Enable Spacer optimization for better solving.
+	p.set("fp.xform.slice", true);
+	p.set("fp.xform.inline_linear", true);
+	p.set("fp.xform.inline_eager", true);
+
+	m_solver.set(p);
+}
+
+void Z3CHCInterface::disablePreProcessing()
+{
+	// Spacer options.
+	// These needs to be set in the solver.
+	// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
+	z3::params p(*m_context);
+	// These are useful for solving problems with arrays and loops.
+	// Use quantified lemma generalizer.
+	p.set("fp.spacer.q3.use_qgen", true);
+	p.set("fp.spacer.mbqi", false);
+	// Ground pobs by using values from a model.
+	p.set("fp.spacer.ground_pobs", false);
+
+	// Disable Spacer optimization for counterexample generation.
+	p.set("fp.xform.slice", false);
+	p.set("fp.xform.inline_linear", false);
+	p.set("fp.xform.inline_eager", false);
+
+	m_solver.set(p);
+}
+
 /**
 Convert a ground refutation into a linear or nonlinear counterexample.
 The counterexample is given as an implication graph of the form
diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h
index 679902b92..e30611f0f 100644
--- a/libsmtutil/Z3CHCInterface.h
+++ b/libsmtutil/Z3CHCInterface.h
@@ -46,6 +46,9 @@ public:
 
 	Z3Interface* z3Interface() const { return m_z3Interface.get(); }
 
+	void enablePreProcessing();
+	void disablePreProcessing();
+
 private:
 	/// Constructs a nonlinear counterexample graph from the refutation.
 	CHCSolverInterface::CexGraph cexGraph(z3::expr const& _proof);
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 130d239b2..e687dffec 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -1128,7 +1128,25 @@ pair<smtutil::CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Exp
 	switch (result)
 	{
 	case smtutil::CheckResult::SATISFIABLE:
+	{
+#ifdef HAVE_Z3
+		// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
+		// We now disable those optimizations and check whether we can still solve the problem.
+		auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
+		solAssert(spacer, "");
+		spacer->disablePreProcessing();
+
+		smtutil::CheckResult resultNoOpt;
+		CHCSolverInterface::CexGraph cexNoOpt;
+		tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
+
+		if (resultNoOpt == smtutil::CheckResult::SATISFIABLE)
+			cex = move(cexNoOpt);
+
+		spacer->enablePreProcessing();
+#endif
 		break;
+	}
 	case smtutil::CheckResult::UNSATISFIABLE:
 		break;
 	case smtutil::CheckResult::UNKNOWN: