diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 16:04:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-02 16:04:43 -0500 |
| commit | 902262c421e52405204b3a95310c8414cc51a5c5 (patch) | |
| tree | 51aa57b918c18854223ee21da8d9b4ff352cba93 /src/smt/smt_engine.cpp | |
| parent | 13f6d4b71a194f74001f7a6fbe92bbb2c5c62813 (diff) | |
Flip the polarity of the argument of get-abduct (#3153)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index df46fc924..914e20b05 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5078,7 +5078,9 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) axioms.push_back(Node::fromExpr(easserts[i])); } std::vector<Node> asserts(axioms.begin(), axioms.end()); - asserts.push_back(Node::fromExpr(conj)); + // negate the conjecture + Node conjn = Node::fromExpr(conj).negate(); + asserts.push_back(conjn); d_sssfVarlist.clear(); d_sssfSyms.clear(); std::string name("A"); |