mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
fix ubuntu build failure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f3d657ebd1
commit
64674386de
|
@ -17,6 +17,7 @@ Author:
|
||||||
Revision History:
|
Revision History:
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
|
#include<typeinfo>
|
||||||
#include"api_context.h"
|
#include"api_context.h"
|
||||||
#include"smtparser.h"
|
#include"smtparser.h"
|
||||||
#include"version.h"
|
#include"version.h"
|
||||||
|
|
|
@ -963,7 +963,6 @@ namespace opt {
|
||||||
unsigned row_id2 = row_ids[i];
|
unsigned row_id2 = row_ids[i];
|
||||||
if (!visited.contains(row_id2)) {
|
if (!visited.contains(row_id2)) {
|
||||||
visited.insert(row_id2);
|
visited.insert(row_id2);
|
||||||
row const& r2 = m_rows[row_id2];
|
|
||||||
b = get_coefficient(row_id2, x);
|
b = get_coefficient(row_id2, x);
|
||||||
if (!b.is_zero()) {
|
if (!b.is_zero()) {
|
||||||
resolve(row_id1, a, row_id2, x);
|
resolve(row_id1, a, row_id2, x);
|
||||||
|
|
Loading…
Reference in a new issue