mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
fix build break based on ambiguous path resolution
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
063b6e9ea5
commit
013127e947
|
@ -576,7 +576,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
|
|||
m_candidates.reset();
|
||||
}
|
||||
|
||||
#include "smt/database.h"
|
||||
#include "database.h"
|
||||
|
||||
void pattern_inference::reduce1_quantifier(quantifier * q) {
|
||||
TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
|
||||
|
|
Loading…
Reference in a new issue