From 58c14ba2f9d22a3040ff466a6250f5faeb867631 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 12 Mar 2024 16:18:39 +0100
Subject: [PATCH] write validation in bv format too

---
 src/sat/smt/intblast_solver.cpp | 64 +++++++++++++++++++++++----------
 1 file changed, 46 insertions(+), 18 deletions(-)

diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 6d0b180d3..1f151c4fe 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -251,19 +251,47 @@ namespace intblast {
             else
                 name_esc = "<none>";
 
-            file << "(set-logic ALL)\n";
-            file << "(set-info :source |\n";
-            file << "    Name: " << name_esc << "\n";
-            file << original_es << "\n|)\n";
+            namespace fs = std::filesystem;
+            static unsigned num_check = 0;
+            num_check += 1;
 
-            m_solver->push();
-            m_solver->assert_expr(es);
-            m_solver->display(file) << "(check-sat)\n";
-            m_solver->pop(1);
+            {
+                fs::path filename = std::string("validation/int-") + std::to_string(num_check) + ".smt2";
+                fs::create_directories(filename.parent_path());
+                IF_VERBOSE(1, verbose_stream() << "validation check written to file " << filename << "\n");
+                std::ofstream file(filename);
 
-            file.close();
+                file << "(set-logic ALL)\n";
+                file << "(set-info :source |\n";
+                file << "    Name: " << name_esc << "\n";
+                file << original_es << "\n|)\n";
 
-            // if (num_check == 68)
+                m_solver->push();
+                m_solver->assert_expr(es);
+                m_solver->display(file) << "(check-sat)\n";
+                m_solver->pop(1);
+
+                file.close();
+            }
+
+            {
+                fs::path filename = std::string("validation/bv-") + std::to_string(num_check) + ".smt2";
+                std::ofstream file(filename);
+
+                file << "(set-logic ALL)\n";
+                file << "(set-info :source |\n";
+                file << "    Name: " << name_esc << "\n";
+                file << original_es << "\n|)\n";
+
+                m_solver->push();
+                m_solver->assert_expr(original_es);
+                m_solver->display(file) << "(check-sat)\n";
+                m_solver->pop(1);
+
+                file.close();
+            }
+
+            // if (num_check == 62)
             //     std::abort();
 
             r = l_false;
@@ -469,10 +497,10 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
-		auto a = eq_internalize(n, sib);
-		auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
-		ctx.mark_relevant(a);
-		ctx.mark_relevant(b);
+                auto a = eq_internalize(n, sib);
+                auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
+                ctx.mark_relevant(a);
+                ctx.mark_relevant(b);
                 add_clause(~a, b, nullptr);
                 return sat::check_result::CR_CONTINUE;
             }
@@ -490,10 +518,10 @@ namespace intblast {
             auto nBv2int = ctx.get_enode(bv2int);
             auto nxModN = ctx.get_enode(xModN);
             if (nBv2int->get_root() != nxModN->get_root()) {
-	      auto a = eq_internalize(nBv2int, nxModN);
-	      ctx.mark_relevant(a);
-              add_unit(a);
-              return sat::check_result::CR_CONTINUE;
+                auto a = eq_internalize(nBv2int, nxModN);
+                ctx.mark_relevant(a);
+                add_unit(a);
+                return sat::check_result::CR_CONTINUE;
             }
         }
         return sat::check_result::CR_DONE;