mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

build errors/warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-16 16:52:18 -07:00
parent 36a2052cca
commit 957c3be02f
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/dotnet/Properties/AssemblyInfo.cs.in
View file

@ -34,5 +34,5 @@ using System.Security.Permissions;
// You can specify all the values or you can default the Build and Revision Numbers // You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below: // by using the '*' as shown below:
// [assembly: AssemblyVersion("4.2.0.0")] // [assembly: AssemblyVersion("4.2.0.0")]
[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] [assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_TWEAK@")]
[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] [assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_TWEAK@")]

6
src/ast/rewriter/rewriter_def.h
View file

@ -82,14 +82,14 @@ template<typename Config>
template<bool ProofGen> template<bool ProofGen>
bool rewriter_tpl<Config>::process_const(app * t0) { bool rewriter_tpl<Config>::process_const(app * t0) {
app_ref t(t0, m()); app_ref t(t0, m());
bool rounds = 0; bool retried = false;
retry: retry:
SASSERT(t->get_num_args() == 0); SASSERT(t->get_num_args() == 0);
br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr); br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
switch (st) { switch (st) {
case BR_FAILED: case BR_FAILED:
if (rounds == 0) { if (!retried) {
result_stack().push_back(t); result_stack().push_back(t);
if (ProofGen) if (ProofGen)
result_pr_stack().push_back(nullptr); // implicit reflexivity result_pr_stack().push_back(nullptr); // implicit reflexivity
@ -112,7 +112,7 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
default: default:
if (is_app(m_r) && to_app(m_r)->get_num_args() == 0) { if (is_app(m_r) && to_app(m_r)->get_num_args() == 0) {
t = to_app(m_r); t = to_app(m_r);
rounds++; retried = true;
goto retry; goto retry;
} }
return false; return false;