mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 06:46:11 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-04 12:51:52 -07:00
parent 70df91bc4e
commit 208cc56861
3 changed files with 11 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -425,6 +425,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
void elim_unconstrained::reduce() {
if (!m_config.m_enabled)
return;
if (m.has_type_vars())
return;
generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
m_inverter.set_model_converter(mc.get());
m_created_compound = true;

24
src/cmd_context/tptp_frontend.cpp
View file

@ -8,20 +8,21 @@
#include <unordered_map>
#include <unordered_set>
#include "util/error_codes.h"
#include "util/rational.h"
#include "util/timeout.h"
#include "util/z3_exception.h"
#include "ast/arith_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/expr_abstract.h"
#include "ast/ast_util.h"
#include "ast/polymorphism_util.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "solver/solver.h"
#include "cmd_context/cmd_context.h"
#include "cmd_context/tptp_frontend.h"
#include "smt/smt_solver.h"
#include "solver/solver.h"
#include "util/error_codes.h"
#include "util/rational.h"
#include "util/timeout.h"
#include "util/z3_exception.h"
bool g_display_statistics = false;
bool g_display_model = false;
@ -2796,16 +2797,7 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
p.parse_input(in, current_file ? current_file : ".");
p.assert_distinct_objects();
// Polymorphic (TF1/TH1) problems are instantiated on demand by
// theory_polymorphism inside the smt core. The strategic solver's tactic
// preprocessing (e.g. unconstrained-subterm elimination) runs before the
// core and can discard a monomorphic instance that only occurs in the
// conjecture, severing it from its polymorphic axiom. Use the plain smt
// solver in that case so instantiation is not defeated by preprocessing.
if (ctx.m().has_type_vars())
ctx.set_solver_factory(mk_smt_solver_factory());
else
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
// Suppress default check-sat output; TPTP frontend reports SZS status explicitly.
std::ostringstream sink;

2
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -945,7 +945,7 @@ class elim_uncnstr_tactic : public tactic {
collect_occs p;
p(*g, m_vars);
disable_quantified(g);
if (m_vars.empty() || recfun::util(m()).has_rec_defs()) {
if (m_vars.empty() || recfun::util(m()).has_rec_defs() || m().has_type_vars()) {
result.push_back(g.get());
// did not increase depth since it didn't do anything.
return;