mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

revert unit propagation of equality literals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-02-18 23:11:03 -08:00
parent 27584d68db
commit a22fb8a96e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/seq_axioms.cpp
View file

@ -70,7 +70,7 @@ literal seq_axioms::mk_literal(expr* _e) {
void seq_axioms::add_clause(expr_ref_vector const& clause) { void seq_axioms::add_clause(expr_ref_vector const& clause) {
expr* a = nullptr, *b = nullptr; expr* a = nullptr, *b = nullptr;
if (clause.size() == 1 && m.is_eq(clause[0], a, b)) { if (false && clause.size() == 1 && m.is_eq(clause[0], a, b)) {
enode* n1 = th.ensure_enode(a); enode* n1 = th.ensure_enode(a);
enode* n2 = th.ensure_enode(b); enode* n2 = th.ensure_enode(b);
justification* js = justification* js =