mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 17:38:45 +00:00
Code Activity

trace reason for undef in arithmetic, enable model generation on THEORY incompleteness, but retain undef result

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-26 12:58:55 -07:00
parent 4995ce1fde
commit 9412890c63
4 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_arith_int.h
View file

@ -1294,8 +1294,10 @@ namespace smt {
}
tout << "max: " << max << ", min: " << min << "\n";);
if (m_params.m_arith_ignore_int)
if (m_params.m_arith_ignore_int) {
TRACE("arith", tout << "Ignore int: give up\n";);
return FC_GIVEUP;
}
if (!gcd_test())
return FC_CONTINUE;