mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
spelling
This commit is contained in:
parent
e2c5e2e39c
commit
ba56bfa656
|
@ -166,9 +166,9 @@ public:
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
class check_sat_using_tactict_cmd : public exec_given_tactic_cmd {
|
class check_sat_using_tactic_cmd : public exec_given_tactic_cmd {
|
||||||
public:
|
public:
|
||||||
check_sat_using_tactict_cmd():
|
check_sat_using_tactic_cmd():
|
||||||
exec_given_tactic_cmd("check-sat-using") {
|
exec_given_tactic_cmd("check-sat-using") {
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -397,7 +397,7 @@ void install_core_tactic_cmds(cmd_context & ctx) {
|
||||||
ctx.insert(alloc(declare_tactic_cmd));
|
ctx.insert(alloc(declare_tactic_cmd));
|
||||||
ctx.insert(alloc(get_user_tactics_cmd));
|
ctx.insert(alloc(get_user_tactics_cmd));
|
||||||
ctx.insert(alloc(help_tactic_cmd));
|
ctx.insert(alloc(help_tactic_cmd));
|
||||||
ctx.insert(alloc(check_sat_using_tactict_cmd));
|
ctx.insert(alloc(check_sat_using_tactic_cmd));
|
||||||
ctx.insert(alloc(apply_tactic_cmd));
|
ctx.insert(alloc(apply_tactic_cmd));
|
||||||
install_tactics(ctx);
|
install_tactics(ctx);
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue