mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

more build errors in debug mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-24 12:57:30 -07:00
parent 48d144a6dd
commit 6300a78b82
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/proofs/proof_utils.h
View file

@ -20,7 +20,9 @@ Revision History:
#ifndef PROOF_UTILS_H_ #ifndef PROOF_UTILS_H_
#define PROOF_UTILS_H_ #define PROOF_UTILS_H_
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bool_rewriter.h"
#include "ast/proofs/proof_checker.h"
/* /*
* iterator, which traverses the proof in depth-first post-order. * iterator, which traverses the proof in depth-first post-order.

9
src/cmd_context/cmd_context.cpp
View file

@ -1053,6 +1053,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
func_decls fs; func_decls fs;
if (!m_func_decls.find(s, fs)) { if (!m_func_decls.find(s, fs)) {
if (num_args == 0) { if (num_args == 0) {
//UNREACHABLE();
throw cmd_exception("unknown constant ", s); throw cmd_exception("unknown constant ", s);
} }
else else
@ -1063,16 +1064,20 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
if (fs.more_than_one()) if (fs.more_than_one())
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s); throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s);
func_decl * f = fs.first(); func_decl * f = fs.first();
if (f == 0) if (f == 0) {
//UNREACHABLE();
throw cmd_exception("unknown constant ", s); throw cmd_exception("unknown constant ", s);
}
if (f->get_arity() != 0) if (f->get_arity() != 0)
throw cmd_exception("invalid function application, missing arguments ", s); throw cmd_exception("invalid function application, missing arguments ", s);
result = m().mk_const(f); result = m().mk_const(f);
} }
else { else {
func_decl * f = fs.find(m(), num_args, args, range); func_decl * f = fs.find(m(), num_args, args, range);
if (f == 0) if (f == 0) {
//UNREACHABLE();
throw cmd_exception("unknown constant ", s); throw cmd_exception("unknown constant ", s);
}
if (well_sorted_check_enabled()) if (well_sorted_check_enabled())
m().check_sort(f, num_args, args); m().check_sort(f, num_args, args);
result = m().mk_app(f, num_args, args); result = m().mk_app(f, num_args, args);