diff --git a/kythe/cxx/verifier/assertions_to_souffle.cc b/kythe/cxx/verifier/assertions_to_souffle.cc
index f341459467..11fc09fcf8 100644
--- a/kythe/cxx/verifier/assertions_to_souffle.cc
+++ b/kythe/cxx/verifier/assertions_to_souffle.cc
@@ -34,11 +34,115 @@ constexpr absl::string_view kGlobalDecls = R"(
 result() :- true
 )";
 }
+
+bool SouffleProgram::LowerSubexpression(AstNode* node) {
+  if (auto* app = node->AsApp()) {
+    auto* tup = app->rhs()->AsTuple();
+    absl::StrAppend(&code_, "[");
+    for (size_t p = 0; p < 5; ++p) {
+      if (p != 0) {
+        absl::StrAppend(&code_, ", ");
+      }
+      if (!LowerSubexpression(tup->element(p))) {
+        return false;
+      }
+    }
+    absl::StrAppend(&code_, "]");
+    return true;
+  } else if (auto* id = node->AsIdentifier()) {
+    absl::StrAppend(&code_, id->symbol());
+    return true;
+  } else if (auto* evar = node->AsEVar()) {
+    if (auto* evc = evar->current()) {
+      return LowerSubexpression(evc);
+    }
+    absl::StrAppend(&code_, "v", FindEVar(evar));
+    return true;
+  } else {
+    LOG(ERROR) << "unknown subexpression kind";
+    return false;
+  }
+}
+
+bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
+                                    const GoalGroup& group) {
+  auto eq_sym = const_cast<SymbolTable&>(symbol_table).intern("=");
+  auto empty_sym = const_cast<SymbolTable&>(symbol_table).intern("");
+#ifdef DEBUG_LOWERING
+  FileHandlePrettyPrinter dprinter(stderr);
+#endif
+  for (const auto& goal : group.goals) {
+#ifdef DEBUG_LOWERING
+    dprinter.Print("goal <");
+    goal->Dump(symbol_table, &dprinter);
+    dprinter.Print(">\n");
+    size_t ccode = code_.size();
+#endif
+    auto* app = goal->AsApp();
+    auto* tup = app->rhs()->AsTuple();
+    if (app->lhs()->AsIdentifier()->symbol() == eq_sym) {
+      auto* evar = tup->element(1)->AsEVar();
+      if (evar == nullptr) {
+        LOG(ERROR) << "expected evar on rhs of eq";
+        return false;
+      }
+      if (auto* range = tup->element(0)->AsRange()) {
+        absl::StrAppend(&code_, ", v", FindEVar(evar), "=[_, ", range->corpus(),
+                        ", ", range->path(), ", ", range->root(), ", _]");
+        // TODO(zarko): derive an anchor relation (will need to convert
+        // range->begin, end to symbols; also need to get the relevant symbols
+        // included in the prelude) or populate the anchor map (would require
+        // sorting input, which is a huge time sink).
+        absl::StrAppend(&code_, ", anchor(", range->begin(), ", ", range->end(),
+                        ", v", FindEVar(evar), ")");
+      } else {
+        auto* oevar = tup->element(0)->AsEVar();
+        if (oevar == nullptr) {
+          LOG(ERROR) << "expected evar or range on lhs of eq";
+          return false;
+        }
+        absl::StrAppend(&code_, ", v", FindEVar(evar), "=v", FindEVar(oevar));
+      }
+    } else {
+      // This is an edge or fact pattern.
+      absl::StrAppend(&code_, ", entry(");
+      for (size_t p = 0; p < 5; ++p) {
+        if (p != 0) {
+          absl::StrAppend(&code_, ", ");
+        }
+        if (p == 2 && tup->element(p)->AsIdentifier() &&
+            tup->element(p)->AsIdentifier()->symbol() == empty_sym) {
+          // Facts have nil vnames in the target position.
+          absl::StrAppend(&code_, "nil");
+          continue;
+        }
+        if (!LowerSubexpression(tup->element(p))) {
+          return false;
+        }
+      }
+      absl::StrAppend(&code_, ")");
+    }
+#ifdef DEBUG_LOWERING
+    dprinter.Print(" => <");
+    dprinter.Print(code_.substr(ccode, code_.size() - ccode));
+    dprinter.Print("> \n");
+#endif
+  }
+  absl::StrAppend(&code_, ".\n");
+  return true;
+}
+
 bool SouffleProgram::Lower(const SymbolTable& symbol_table,
                            const std::vector<GoalGroup>& goal_groups) {
   code_ = emit_prelude_ ? std::string(kGlobalDecls) : "";
   CHECK_LE(goal_groups.size(), 1) << "(unimplemented)";
-  absl::StrAppend(&code_, ".\n");
+  if (goal_groups.size() == 0) {
+    absl::StrAppend(&code_, ".\n");
+    return true;
+  }
+  for (const auto& group : goal_groups) {
+    if (!LowerGoalGroup(symbol_table, group)) return false;
+  }
   return true;
 }
 }  // namespace kythe::verifier
diff --git a/kythe/cxx/verifier/assertions_to_souffle.h b/kythe/cxx/verifier/assertions_to_souffle.h
index 1e6b4fc979..43903b6377 100644
--- a/kythe/cxx/verifier/assertions_to_souffle.h
+++ b/kythe/cxx/verifier/assertions_to_souffle.h
@@ -19,6 +19,7 @@
 
 #include <string>
 
+#include "absl/container/flat_hash_map.h"
 #include "absl/strings/string_view.h"
 #include "kythe/cxx/verifier/assertion_ast.h"
 
@@ -39,11 +40,25 @@ class SouffleProgram {
   void set_emit_prelude(bool emit_prelude) { emit_prelude_ = emit_prelude; }
 
  private:
+  /// \brief Lowers `node`.
+  bool LowerSubexpression(AstNode* node);
+
+  /// \brief Lowers `group`.
+  bool LowerGoalGroup(const SymbolTable& symbol_table, const GoalGroup& group);
+
+  /// \return a stable short name for `ev`.
+  size_t FindEVar(EVar* ev) {
+    return evars_.try_emplace(ev, evars_.size()).first->second;
+  }
+
   /// The current finished code buffer.
   std::string code_;
 
   /// Whether to emit the prelude.
   bool emit_prelude_ = true;
+
+  /// Known evars.
+  absl::flat_hash_map<EVar*, size_t> evars_;
 };
 
 }  // namespace kythe::verifier
diff --git a/kythe/cxx/verifier/souffle_interpreter.cc b/kythe/cxx/verifier/souffle_interpreter.cc
index 96982358b1..2ba246bd97 100644
--- a/kythe/cxx/verifier/souffle_interpreter.cc
+++ b/kythe/cxx/verifier/souffle_interpreter.cc
@@ -35,7 +35,8 @@ class KytheReadStream : public souffle::ReadStream {
   explicit KytheReadStream(
       const std::map<std::string, std::string>& rw_operation,
       souffle::SymbolTable& symbol_table, souffle::RecordTable& record_table,
-      const AnchorMap& anchors, const Database& database)
+      const AnchorMap& anchors, const Database& database,
+      const SymbolTable& dst)
       : souffle::ReadStream(rw_operation, symbol_table, record_table),
         anchors_(anchors),
         database_(database) {
@@ -46,6 +47,20 @@ class KytheReadStream : public souffle::ReadStream {
       database_it_ = database_.cbegin();
       anchor_it_ = anchors_.cend();
     }
+#ifdef DEBUG_LOWERING
+    FileHandlePrettyPrinter dprinter(stderr);
+    for (const auto& d : database) {
+      dprinter.Print("- ");
+      d->Dump(dst, &dprinter);
+      dprinter.Print("\n");
+    }
+    for (const auto& a : anchors) {
+      dprinter.Print(
+          absl::StrCat("@ ", a.first.first, ", ", a.first.second, " "));
+      a.second->Dump(dst, &dprinter);
+      dprinter.Print("\n");
+    }
+#endif
     std::array<souffle::RamDomain, 5> fields = {0, 0, 0, 0, 0};
     empty_vname_ = record_table.pack(fields.data(), fields.size());
   }
@@ -60,6 +75,7 @@ class KytheReadStream : public souffle::ReadStream {
       tuple[0] = recordTable.pack(vname, 5);
       tuple[1] = t->element(1)->AsIdentifier()->symbol();
       if (auto* id = t->element(2)->AsIdentifier(); id != nullptr) {
+        // TODO(zarko): this should possibly be an explicit nil.
         tuple[2] = id->symbol();
       } else {
         CopyVName(t->element(2)->AsApp()->rhs()->AsTuple(), vname);
@@ -102,15 +118,16 @@ class KytheReadStream : public souffle::ReadStream {
 
 class KytheReadStreamFactory : public souffle::ReadStreamFactory {
  public:
-  KytheReadStreamFactory(const AnchorMap& anchors, const Database& database)
-      : anchors_(anchors), database_(database) {}
+  KytheReadStreamFactory(const AnchorMap& anchors, const Database& database,
+                         const SymbolTable& dst)
+      : anchors_(anchors), database_(database), dst_(dst) {}
 
   souffle::Own<souffle::ReadStream> getReader(
       const std::map<std::string, std::string>& rw_operation,
       souffle::SymbolTable& symbol_table,
       souffle::RecordTable& record_table) override {
-    return souffle::mk<KytheReadStream>(rw_operation, symbol_table,
-                                        record_table, anchors_, database_);
+    return souffle::mk<KytheReadStream>(
+        rw_operation, symbol_table, record_table, anchors_, database_, dst_);
   }
 
   const std::string& getName() const override {
@@ -121,6 +138,7 @@ class KytheReadStreamFactory : public souffle::ReadStreamFactory {
  private:
   const AnchorMap& anchors_;
   const Database& database_;
+  const SymbolTable& dst_;
 };
 
 class KytheWriteStream : public souffle::WriteStream {
@@ -190,10 +208,12 @@ SouffleResult RunSouffle(const SymbolTable& symbol_table,
   souffle::IOSystem::getInstance().registerWriteStreamFactory(
       write_stream_factory);
   souffle::IOSystem::getInstance().registerReadStreamFactory(
-      std::make_shared<KytheReadStreamFactory>(anchors, database));
+      std::make_shared<KytheReadStreamFactory>(anchors, database,
+                                               symbol_table));
   auto ram_tu = souffle::ParseTransform(absl::StrCat(
       program.code(), ".output result(IO=kythe, id=", output_id, ")\n"));
   if (ram_tu == nullptr) {
+    LOG(ERROR) << "no ram_tu for program <" << program.code() << ">";
     return result;
   }
   souffle::Own<souffle::interpreter::Engine> interpreter(
diff --git a/kythe/cxx/verifier/verifier.cc b/kythe/cxx/verifier/verifier.cc
index 37ae2d4b71..dc4a0afb73 100644
--- a/kythe/cxx/verifier/verifier.cc
+++ b/kythe/cxx/verifier/verifier.cc
@@ -1108,7 +1108,7 @@ static bool EncodedFactHasValidForm(Verifier* cxt, AstNode* a) {
 }
 
 Verifier::InternedVName Verifier::InternVName(AstNode* node) {
-  auto* tuple = node->AsTuple();
+  auto* tuple = node->AsApp()->rhs()->AsTuple();
   return {tuple->element(0)->AsIdentifier()->symbol(),
           tuple->element(1)->AsIdentifier()->symbol(),
           tuple->element(2)->AsIdentifier()->symbol(),
@@ -1152,11 +1152,10 @@ bool Verifier::ProcessFactTupleForFastSolver(Tuple* tuple) {
 }
 
 bool Verifier::PrepareDatabase() {
-  if (database_prepared_) {
+  if (database_prepared_ || use_fast_solver_) {
+    LOG(WARNING) << "PrepareDatabase() called when fast solver was enabled";
     return true;
   }
-  CHECK(!use_fast_solver_)
-      << "This configuration is not supported when --use_fast_solver is on.";
   // TODO(zarko): Make this configurable.
   FileHandlePrettyPrinter printer(stderr);
   // First, sort the tuples. As an invariant, we know they will be of the form
diff --git a/kythe/cxx/verifier/verifier_unit_test.cc b/kythe/cxx/verifier/verifier_unit_test.cc
index 9fae91314f..2009d821cd 100644
--- a/kythe/cxx/verifier/verifier_unit_test.cc
+++ b/kythe/cxx/verifier/verifier_unit_test.cc
@@ -132,8 +132,7 @@ TEST(VerifierUnitTest, EmptyVnameIsNotWellFormed) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, NoRulesIsOk) {
-  Verifier v;
+TEST_P(VerifierTest, NoRulesIsOk) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
   source { root: "1" }
   fact_name: "testname"
@@ -200,8 +199,7 @@ entries {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, EdgesCanSupplyMultipleOrdinals) {
-  Verifier v;
+TEST_P(VerifierTest, EdgesCanSupplyMultipleOrdinals) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
   source { root: "1" }
   edge_kind: "somekind"
@@ -220,8 +218,7 @@ entries {
   ASSERT_TRUE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, EdgesCanSupplyMultipleDotOrdinals) {
-  Verifier v;
+TEST_P(VerifierTest, EdgesCanSupplyMultipleDotOrdinals) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
   source { root: "1" }
   edge_kind: "somekind.42"
@@ -277,8 +274,7 @@ TEST(VerifierUnitTest, OnlyTargetIsWrongDotOrdinal) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, MissingAnchorTextFails) {
-  Verifier v;
+TEST_P(VerifierTest, MissingAnchorTextFails) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(entries {
 #- @text defines SomeNode
   source { root: "1" }
@@ -287,8 +283,7 @@ TEST(VerifierUnitTest, MissingAnchorTextFails) {
 })"));
 }
 
-TEST(VerifierUnitTest, AmbiguousAnchorTextFails) {
-  Verifier v;
+TEST_P(VerifierTest, AmbiguousAnchorTextFails) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(entries {
 #- @text defines SomeNode
 # text text
@@ -298,8 +293,7 @@ TEST(VerifierUnitTest, AmbiguousAnchorTextFails) {
 })"));
 }
 
-TEST(VerifierUnitTest, GenerateAnchorEvarFailsOnEmptyDB) {
-  Verifier v;
+TEST_P(VerifierTest, GenerateAnchorEvarFailsOnEmptyDB) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(
 #- @text defines SomeNode
 # text
@@ -308,8 +302,7 @@ TEST(VerifierUnitTest, GenerateAnchorEvarFailsOnEmptyDB) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, OffsetsVersusRuleBlocks) {
-  Verifier v;
+TEST_P(VerifierTest, OffsetsVersusRuleBlocks) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(
 #- @text defines SomeNode
 #- @+2text defines SomeNode
@@ -320,16 +313,14 @@ TEST(VerifierUnitTest, OffsetsVersusRuleBlocks) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, ZeroRelativeLineReferencesDontWork) {
-  Verifier v;
+TEST_P(VerifierTest, ZeroRelativeLineReferencesDontWork) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #- @+0text defines SomeNode
 # text
 )"));
 }
 
-TEST(VerifierUnitTest, NoMatchingInsideGoalComments) {
-  Verifier v;
+TEST_P(VerifierTest, NoMatchingInsideGoalComments) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #- @+1text defines SomeNode
 #- @text defines SomeNode
@@ -337,23 +328,21 @@ TEST(VerifierUnitTest, NoMatchingInsideGoalComments) {
 )"));
 }
 
-TEST(VerifierUnitTest, OutOfBoundsRelativeLineReferencesDontWork) {
-  Verifier v;
+TEST_P(VerifierTest, OutOfBoundsRelativeLineReferencesDontWork) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #- @+2text defines SomeNode
 # text
 )"));
 }
 
-TEST(VerifierUnitTest, EndOfFileAbsoluteLineReferencesWork) {
-  Verifier v;
+TEST_P(VerifierTest, EndOfFileAbsoluteLineReferencesWork) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(
 #- @:3text defines SomeNode
 # text
 )"));
 }
 
-TEST(VerifierUnitTest, OutOfBoundsAbsoluteLineReferencesDontWork) {
+TEST_P(VerifierTest, OutOfBoundsAbsoluteLineReferencesDontWork) {
   Verifier v;
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #- @:4text defines SomeNode
@@ -361,24 +350,21 @@ TEST(VerifierUnitTest, OutOfBoundsAbsoluteLineReferencesDontWork) {
 )"));
 }
 
-TEST(VerifierUnitTest, ZeroAbsoluteLineReferencesDontWork) {
-  Verifier v;
+TEST_P(VerifierTest, ZeroAbsoluteLineReferencesDontWork) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #- @:0text defines SomeNode
 # text
 )"));
 }
 
-TEST(VerifierUnitTest, SameAbsoluteLineReferencesDontWork) {
-  Verifier v;
+TEST_P(VerifierTest, SameAbsoluteLineReferencesDontWork) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #- @:1text defines SomeNode
 # text
 )"));
 }
 
-TEST(VerifierUnitTest, HistoricalAbsoluteLineReferencesDontWork) {
-  Verifier v;
+TEST_P(VerifierTest, HistoricalAbsoluteLineReferencesDontWork) {
   ASSERT_FALSE(v.LoadInlineProtoFile(R"(
 #
 #- @:1text defines SomeNode
@@ -386,8 +372,7 @@ TEST(VerifierUnitTest, HistoricalAbsoluteLineReferencesDontWork) {
 )"));
 }
 
-TEST(VerifierUnitTest, ParseLiteralString) {
-  Verifier v;
+TEST_P(VerifierTest, ParseLiteralString) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(
 #- @"text" defines SomeNode
 # text
@@ -396,8 +381,7 @@ TEST(VerifierUnitTest, ParseLiteralString) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, ParseLiteralStringWithSpace) {
-  Verifier v;
+TEST_P(VerifierTest, ParseLiteralStringWithSpace) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(
 #- @"text txet" defines SomeNode
 # text txet
@@ -406,8 +390,7 @@ TEST(VerifierUnitTest, ParseLiteralStringWithSpace) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, ParseLiteralStringWithEscape) {
-  Verifier v;
+TEST_P(VerifierTest, ParseLiteralStringWithEscape) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(
 #- @"text \"txet\" ettx" defines SomeNode
 # text "txet" ettx
@@ -416,8 +399,7 @@ TEST(VerifierUnitTest, ParseLiteralStringWithEscape) {
   ASSERT_FALSE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, GenerateStartOffsetEVar) {
-  Verifier v;
+TEST_P(VerifierTest, GenerateStartOffsetEVar) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #- ANode.loc/start @^text
 ##text (line 3 column 2 offset 38-42)
@@ -446,8 +428,7 @@ fact_value: ""
   ASSERT_TRUE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, GenerateStartOffsetEVarRelativeLine) {
-  Verifier v;
+TEST_P(VerifierTest, GenerateStartOffsetEVarRelativeLine) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #- ANode.loc/start @^+22text
 source { root:"1" }
@@ -476,8 +457,7 @@ fact_value: ""
   ASSERT_TRUE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, GenerateEndOffsetEVarAbsoluteLine) {
-  Verifier v;
+TEST_P(VerifierTest, GenerateEndOffsetEVarAbsoluteLine) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #-   ANode.loc/end @$:24text
 source { root:"1" }
@@ -506,8 +486,7 @@ fact_value: ""
   ASSERT_TRUE(v.VerifyAllGoals());
 }
 
-TEST(VerifierUnitTest, GenerateEndOffsetEVar) {
-  Verifier v;
+TEST_P(VerifierTest, GenerateEndOffsetEVar) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #-   ANode.loc/end @$text
 ##text (line 3 column 2 offset 38-42)
@@ -536,6 +515,7 @@ fact_value: ""
   ASSERT_TRUE(v.VerifyAllGoals());
 }
 
+// TODO(zarko): See comments in souffle_interpreter re: the anchor() relation.
 TEST(VerifierUnitTest, GenerateAnchorEvar) {
   Verifier v;
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {