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

fix for #1202

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-13 09:25:46 -07:00
parent c4083c367a
commit 347ea50b93
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -8420,6 +8420,7 @@ namespace smt {
// Check agreement between integer and string theories for the term a = (str.to-int S). // Check agreement between integer and string theories for the term a = (str.to-int S).
// Returns true if axioms were added, and false otherwise. // Returns true if axioms were added, and false otherwise.
bool theory_str::finalcheck_str2int(app * a) { bool theory_str::finalcheck_str2int(app * a) {
SASSERT(u.str.is_stoi(a));
bool axiomAdd = false; bool axiomAdd = false;
context & ctx = get_context(); context & ctx = get_context();
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -8446,7 +8447,10 @@ namespace smt {
} }
} else { } else {
TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;); TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;);
NOT_IMPLEMENTED_YET(); expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m);
literal is_zero_l = mk_literal(is_zero);
axiomAdd = true;
// NOT_IMPLEMENTED_YET();
} }
return axiomAdd; return axiomAdd;