mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 01:03:38 -07:00
parent 399cf75ad4
commit 296a97d0d3
4 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/dyn_ack.cpp
View file

@ -145,6 +145,7 @@ namespace smt {
if (m_eq1->get_arg(1) == m_app1) p1 = m.mk_symmetry(p1);
p2 = m.mk_hypothesis(m_eq2);
if (m_eq2->get_arg(0) == m_app2) p2 = m.mk_symmetry(p2);
(void)m_r;
SASSERT(m.is_eq(m.get_fact(p1), x, y) && x == m_app1 && y == m_r);
SASSERT(m.is_eq(m.get_fact(p2), x, y) && x == m_r && y == m_app2);
p3 = m.mk_transitivity(p1, p2);

3
src/smt/theory_lra.cpp
View file

@ -2513,7 +2513,6 @@ public:
void mk_bound_axiom(lp_api::bound& b1, lp_api::bound& b2) {
theory_var v = b1.get_var();
literal l1(b1.get_bv());
literal l2(b2.get_bv());
rational const& k1 = b1.get_value();
@ -2521,7 +2520,7 @@ public:
lp_api::bound_kind kind1 = b1.get_bound_kind();
lp_api::bound_kind kind2 = b2.get_bound_kind();
bool v_is_int = b1.is_int();
SASSERT(v == b2.get_var());
SASSERT(b1.get_var() == b2.get_var());
if (k1 == k2 && kind1 == kind2) return;
SASSERT(k1 != k2 || kind1 != kind2);
parameter coeffs[3] = { parameter(symbol("farkas")),

6
src/solver/parallel_tactic.cpp
View file

@ -236,7 +236,7 @@ class parallel_tactic : public tactic {
vector<cube_var> split_cubes(unsigned n) {
vector<cube_var> result;
while (n-- > 0 && !m_cubes.empty()) {
for (expr* c : m_cubes.back().cube()) SASSERT(c);
DEBUG_CODE(for (expr* c : m_cubes.back().cube()) SASSERT(c););
result.push_back(m_cubes.back());
m_cubes.pop_back();
@ -246,7 +246,7 @@ class parallel_tactic : public tactic {
void set_cubes(vector<cube_var>& c) {
m_cubes.reset();
for (auto & cb : c) for (expr* e : cb.cube()) SASSERT(e);
DEBUG_CODE(for (auto & cb : c) for (expr* e : cb.cube()) SASSERT(e););
m_cubes.append(c);
}
@ -517,7 +517,7 @@ private:
if (conquer) {
is_sat = conquer->check_sat(c);
}
for (expr* e : c) SASSERT(e);
DEBUG_CODE(for (expr* e : c) SASSERT(e););
switch (is_sat) {
case l_false:
cutoff = c.size();

2
src/test/lp/lp.cpp
View file

@ -43,7 +43,7 @@
#include "math/lp/lar_solver.h"
#include "math/lp/numeric_pair.h"
#include "math/lp/binary_heap_upair_queue.h"
#include "math/lp/stacked_value.h"
#include "util/stacked_value.h"
#include "math/lp/u_set.h"
#include "util/stopwatch.h"
#include <cstdlib>