projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2ba8c85) | patch
Fix disequality between seq.unit terms (#5880)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 8 Feb 2021 21:55:32 +0000 (15:55 -0600)
committerGitHub <noreply@github.com>
Mon, 8 Feb 2021 21:55:32 +0000 (15:55 -0600)
commitca9705cf0785e3a81fc25995df0bc3dc76e3bd9f
tree89359d3de3099cae4557aabc2a23f342098b09c6tree
parent2ba8c852864ecb2eea3be2253fb80af1328de158commit | diff
Fix disequality between seq.unit terms (#5880)

This adds a missing inference for disequality between seq.unit terms, which was not handled previously.

Fixes #5666.
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/core_solver.h diff | blob | history
src/theory/strings/infer_info.cpp diff | blob | history
src/theory/strings/infer_info.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue5666-orig-unit-deq.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/issue5666-unit-deq.smt2 [new file with mode: 0644] blob