3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

modify offset check to accept linear expressions over numerals. Codeplex issue 81

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-02 17:50:29 -08:00
parent 23313e5bdc
commit b1b349f496

View file

@ -310,6 +310,8 @@ struct check_logic::imp {
return false;
non_numeral = arg;
}
if (non_numeral == 0)
return true;
if (is_diff_var(non_numeral))
return true;
if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))