mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

fix bugs reported by Anvesh

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-23 04:07:08 +03:00
parent 0a964c324e
commit fd1f4b9191
3 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3.py
View file

@ -6449,7 +6449,7 @@ class Tactic:
def _to_goal(a): def _to_goal(a):
if isinstance(a, BoolRef): if isinstance(a, BoolRef):
goal = Goal() goal = Goal(a.ctx)
goal.add(a) goal.add(a)
return goal return goal
else: else:

7
src/smt/diff_logic.h
View file

@ -820,6 +820,7 @@ public:
} }
} }
private:
// Update the assignment of variable v, that is, // Update the assignment of variable v, that is,
// m_assignment[v] += inc // m_assignment[v] += inc
// This method also stores the old value of v in the assignment stack. // This method also stores the old value of v in the assignment stack.
@ -829,6 +830,12 @@ public:
m_assignment[v] += inc; m_assignment[v] += inc;
} }
public:
void inc_assignment(dl_var v, numeral const& inc) {
m_assignment[v] += inc;
}
struct every_var_proc { struct every_var_proc {
bool operator()(dl_var v) const { bool operator()(dl_var v) const {

3
src/smt/theory_utvpi_def.h
View file

@ -752,7 +752,8 @@ namespace smt {
for (unsigned j = 0; j < zero_v.size(); ++j) { for (unsigned j = 0; j < zero_v.size(); ++j) {
int v = zero_v[j]; int v = zero_v[j];
m_graph.acc_assignment(v, numeral(-1));
m_graph.inc_assignment(v, numeral(-1));
th_var k = from_var(v); th_var k = from_var(v);
if (!is_parity_ok(k)) { if (!is_parity_ok(k)) {
todo.push_back(k); todo.push_back(k);