mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c4829dfa22
commit
aad09816cb
|
@ -1,4 +1,3 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
|
@ -26,8 +25,8 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
|
|||
<< "(assert " << str << ")\n";
|
||||
std::istringstream is(buffer.str());
|
||||
VERIFY(parse_smt2_commands(ctx, is));
|
||||
ENSURE(ctx.begin_assertions() != ctx.end_assertions());
|
||||
result = *ctx.begin_assertions();
|
||||
ENSURE(!ctx.assertions().empty());
|
||||
result = ctx.assertions().get(0);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
@ -25,8 +25,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
|
|||
<< "(assert " << str << ")\n";
|
||||
std::istringstream is(buffer.str());
|
||||
VERIFY(parse_smt2_commands(ctx, is));
|
||||
ENSURE(ctx.begin_assertions() != ctx.end_assertions());
|
||||
result = *ctx.begin_assertions();
|
||||
result = ctx.assertions().get(0);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
@ -37,8 +37,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
|
|||
<< "(assert " << str << ")\n";
|
||||
std::istringstream is(buffer.str());
|
||||
VERIFY(parse_smt2_commands(ctx, is));
|
||||
ENSURE(ctx.begin_assertions() != ctx.end_assertions());
|
||||
result = *ctx.begin_assertions();
|
||||
result = ctx.assertions().get(0);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
@ -131,8 +131,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
|
|||
<< "(assert " << str << ")\n";
|
||||
std::istringstream is(buffer.str());
|
||||
VERIFY(parse_smt2_commands(ctx, is));
|
||||
ENSURE(ctx.begin_assertions() != ctx.end_assertions());
|
||||
result = *ctx.begin_assertions();
|
||||
result = ctx.assertions().get(0);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue