mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

hack to filter out Boogie axioms with large "distinct" predicates that cause legacy solver death

Browse source
This commit is contained in:
Ken McMillan 2014-04-06 13:01:20 -07:00
parent 2b492f04f6
commit 58ffffe4d4
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/duality/duality.h
View file

@ -253,6 +253,10 @@ protected:
}
void assert_axiom(const expr &axiom){
// 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;
islvr->AssertInterpolationAxiom(axiom);
}