mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
removed distinct predicate hack
This commit is contained in:
parent
de81db9a3b
commit
60ef669fbc
|
@ -253,10 +253,12 @@ protected:
|
|||
}
|
||||
|
||||
void assert_axiom(const expr &axiom){
|
||||
#if 0
|
||||
// HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them
|
||||
if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct)
|
||||
if(axiom.num_args() > 10)
|
||||
return;
|
||||
#endif
|
||||
islvr->AssertInterpolationAxiom(axiom);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue