projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 617f1b0) | patch
Abort if in conflict in enumerative instantiation (#4298)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Apr 2020 06:28:18 +0000 (01:28 -0500)
committerGitHub <noreply@github.com>
Wed, 15 Apr 2020 06:28:18 +0000 (01:28 -0500)
commitc808605ef15eb79f9ddc2d1a2b4f6dd052530877
treeb2aa5750a536fe979da32d2e755c3dbac3a389cetree
parent617f1b0fe93e077d6e76e03dcf1a75730740fe27commit | diff
Abort if in conflict in enumerative instantiation (#4298)

In very rare cases, quantifiers engine can be the first to detect a quantifier-free conflict while constructing term indices. When this occurs, instantiation modules can quit immediately. This was not happening in a case of enumerative instantiation.

Fixes #4293.
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history