Inconsistent verdict on SMT-LIB queries (compared to z3 and CVC5)

[nicolasAmat]

Hi,

I got UNSAT verdicts on the following queries from the SMT-LIB repository (non-incremental/QF-LIA):

• 20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem_2__003.smt2.slack.smt2
• 20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem__009.smt2.slack.smt2
• 20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem__017.smt2.slack.smt2

I compared the results with two SMT solvers (z3 and cvc5) and both returned SAT.

I ran the following command : ./run-amaya.py --fast -O all --verbose get-sat <query.smt2>.

Perhaps I am missing something in the use or configuration of Amaya.

Bellow is the output from Amaya:

[2024/08/19 16:43:01](INFO): Executing evaluation procedure with configuration: SolverConfig(solution_domain=<SolutionDomain.INTEGERS: 1>, minimization_method=<MinimizationAlgorithms.HOPCROFT: 1>, backend_type=<BackendType.MTBDD: 2>, track_operation_runtime=False, track_state_semantics=False, optimizations=OptimizationsConfig(allow_sharding=False, simplify_variable_bounds=True, rewrite_existential_equations_via_gcd=True, push_negation_towards_atoms=True, do_interval_analysis=True, do_light_sat_reasoning=True, do_lazy_evaluation=True, do_miniscoping=True, do_gcd_divide=True, rewrite_congruences_with_unbound_terms=True, detect_isomorphic_conflicts=True, linearize_similar_mod_terms=True, reorder_conjunctions=True, do_interval_reasonining_twice=True, linearize_congruences=True, optimize_bottom_quantifiers=True), vis_display_only_free_vars=False, print_stats=False, preprocessing=PreprocessingConfig(perform_prenexing=False, perform_antiprenexing=False, disambiguate_variables=True, assign_new_variable_names=False, use_congruences_when_rewriting_modulo=True, use_two_vars_when_rewriting_nonlin_terms=False, show_preprocessed_formula=False, display_var_table=False), current_formula_path='/home/nicolas.amat/Presburger-automata/Experimental_Evaluation/non-incremental/QF_LIA/20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem_2__003.smt2.slack.smt2', export_counter=0, disambiguation_scope_separator='_', report_highly_effective_minimizations=False, max_allowed_states=None)
[2024/08/19 16:43:01](INFO): [Preprocessing] Rewriting if-then-else expressions.
[2024/08/19 16:43:01](INFO): First pass stats:
[2024/08/19 16:43:01](INFO): Replaced 0 forall quantifiers with exists.
[2024/08/19 16:43:01](INFO): Expanded 0 implications.
[2024/08/19 16:43:01](INFO): Entering the third preprocessing pass: double negation removal.
[2024/08/19 16:43:01](INFO): Removed 0 negation pairs.
[2024/08/19 16:43:01](INFO): Condensing atomic relation ASTs into AST leaves.
[2024/08/19 16:43:01](INFO): Preprocessing resulted in the following AST: ['and', Relation(-1.Var(id=1) <= 0), Relation(-1.Var(id=2) <= 0), Relation(-1.Var(id=3) <= 0), Relation(-1.Var(id=4) <= 0), Relation(-1.Var(id=5) <= 0), Relation(-1.Var(id=6) <= 0), Relation(-1.Var(id=7) <= 0), Relation(-1.Var(id=8) <= 0), Relation(-1.Var(id=9) <= 0), Relation(-1.Var(id=10) <= 0), Relation(-1.Var(id=11) <= 0), Relation(-1.Var(id=12) <= 0), Relation(-1.Var(id=13) <= 0), Relation(-1.Var(id=14) <= 0), Relation(-1.Var(id=15) <= 0), Relation(-1.Var(id=16) <= 0), Relation(-1.Var(id=17) <= 0), Relation(-1.Var(id=18) <= 0), Relation(-1.Var(id=19) <= 0), Relation(-1.Var(id=20) <= 0), Relation(-1.Var(id=21) <= 0), Relation(-1.Var(id=22) <= 0), Relation(-1.Var(id=23) <= 0), Relation(-1.Var(id=24) <= 0), Relation(-1.Var(id=25) <= 0), Relation(-1.Var(id=26) <= 0), Relation(-1.Var(id=27) <= 0), Relation(-1.Var(id=28) <= 0), Relation(-1.Var(id=29) <= 0), Relation(-1.Var(id=30) <= 0), Relation(-1.Var(id=31) <= 0), Relation(-1.Var(id=32) <= 0), Relation(-1.Var(id=33) <= 0), Relation(-1.Var(id=34) <= 0), Relation(-1.Var(id=35) <= 0), Relation(-1.Var(id=36) <= 0), Relation(-1.Var(id=37) <= 0), Relation(-1.Var(id=38) <= 0), Relation(-1.Var(id=39) <= 0), Relation(-1.Var(id=40) <= 0), Relation(-1.Var(id=41) <= 0), Relation(-1.Var(id=42) <= 0), Relation(-1.Var(id=43) <= 0), Relation(-1.Var(id=44) <= 0), Relation(-1.Var(id=45) <= 0), Relation(-1.Var(id=46) <= 0), Relation(-1.Var(id=47) <= 0), Relation(-1.Var(id=48) <= 0), Relation(-1.Var(id=49) <= 0), Relation(-1.Var(id=50) <= 0), Relation(-1.Var(id=51) <= 0), Relation(-1.Var(id=52) <= 0), Relation(-1.Var(id=53) <= 0), Relation(-1.Var(id=54) <= 0), Relation(-1.Var(id=55) <= 0), Relation(-1.Var(id=56) <= 0), Relation(-1.Var(id=57) <= 0), Relation(-1.Var(id=58) <= 0), Relation(-1.Var(id=59) <= 0), Relation(-1.Var(id=60) <= 0), Relation(-1.Var(id=61) <= 0), Relation(-1.Var(id=62) <= 0), Relation(-1.Var(id=63) <= 0), Relation(-1.Var(id=64) <= 0), Relation(-1.Var(id=65) <= 0), Relation(-1.Var(id=66) <= 0), Relation(-1.Var(id=67) <= 0), Relation(-1.Var(id=68) <= 0), Relation(-1.Var(id=69) <= 0), Relation(-1.Var(id=70) <= 0), Relation(-1.Var(id=71) <= 0), Relation(-1.Var(id=72) <= 0), Relation(-1.Var(id=73) <= 0), Relation(-1.Var(id=74) <= 0), Relation(-1.Var(id=75) <= 0), Relation(-1.Var(id=76) <= 0), Relation(-1.Var(id=77) <= 0), Relation(-1.Var(id=78) <= 0), Relation(-1.Var(id=79) <= 0), Relation(-1.Var(id=80) <= 0), Relation(-1.Var(id=81) <= 0), Relation(-1.Var(id=82) <= 0), Relation(-1.Var(id=83) <= 0), Relation(-1.Var(id=84) <= 0), Relation(-1.Var(id=85) <= 0), Relation(-1.Var(id=86) <= 0), Relation(-1.Var(id=87) <= 0), Relation(-1.Var(id=88) <= 0), Relation(-1.Var(id=89) <= 0), Relation(-1.Var(id=90) <= 0), Relation(+1.Var(id=1) -1.Var(id=2) -1.Var(id=3) +1.Var(id=4) +1.Var(id=5) -1.Var(id=6) +2.Var(id=7) -2.Var(id=8) -1.Var(id=9) +1.Var(id=10) +1.Var(id=11) -1.Var(id=12) +1.Var(id=13) -1.Var(id=14) +1.Var(id=15) -1.Var(id=16) -1.Var(id=17) +1.Var(id=18) -1.Var(id=19) +1.Var(id=20) -1.Var(id=21) +1.Var(id=22) -1.Var(id=23) +1.Var(id=24) -1.Var(id=25) +1.Var(id=26) +1.Var(id=27) -1.Var(id=28) +1.Var(id=29) -1.Var(id=30) +1.Var(id=31) -1.Var(id=32) -1.Var(id=33) +1.Var(id=34) -1.Var(id=35) +1.Var(id=36) +1.Var(id=37) -1.Var(id=38) +1.Var(id=39) -1.Var(id=40) <= -1), Relation(+1.Var(id=1) -1.Var(id=2) +1.Var(id=3) -1.Var(id=4) +2.Var(id=15) -2.Var(id=16) +1.Var(id=23) -1.Var(id=24) +1.Var(id=27) -1.Var(id=28) +1.Var(id=31) -1.Var(id=32) -1.Var(id=35) +1.Var(id=36) +2.Var(id=37) -2.Var(id=38) +1.Var(id=39) -1.Var(id=40) +1.Var(id=41) -1.Var(id=42) -1.Var(id=43) +1.Var(id=44) +1.Var(id=45) -1.Var(id=46) -1.Var(id=47) +1.Var(id=48) -1.Var(id=49) +1.Var(id=50) -1.Var(id=51) +1.Var(id=52) +1.Var(id=53) -1.Var(id=54) -1.Var(id=55) +1.Var(id=56) -1.Var(id=57) +1.Var(id=58) -1.Var(id=59) +1.Var(id=60) +1.Var(id=61) -1.Var(id=62) <= 0), Relation(+1.Var(id=1) -1.Var(id=2) +1.Var(id=3) -1.Var(id=4) -1.Var(id=5) +1.Var(id=6) -1.Var(id=7) +1.Var(id=8) -1.Var(id=11) +1.Var(id=12) +2.Var(id=15) -2.Var(id=16) -1.Var(id=19) +1.Var(id=20) -1.Var(id=21) +1.Var(id=22) +2.Var(id=27) -2.Var(id=28) +1.Var(id=35) -1.Var(id=36) -1.Var(id=39) +1.Var(id=40) +1.Var(id=47) -1.Var(id=48) -1.Var(id=49) +1.Var(id=50) -1.Var(id=55) +1.Var(id=56) +1.Var(id=61) -1.Var(id=62) +1.Var(id=63) -1.Var(id=64) -1.Var(id=65) +1.Var(id=66) -1.Var(id=67) +1.Var(id=68) -1.Var(id=69) +1.Var(id=70) <= 0), Relation(+1.Var(id=5) -1.Var(id=6) -1.Var(id=17) +1.Var(id=18) -1.Var(id=23) +1.Var(id=24) +1.Var(id=25) -1.Var(id=26) +1.Var(id=33) -1.Var(id=34) +1.Var(id=35) -1.Var(id=36) +1.Var(id=37) -1.Var(id=38) -2.Var(id=39) +2.Var(id=40) +1.Var(id=41) -1.Var(id=42) -1.Var(id=43) +1.Var(id=44) +2.Var(id=47) -2.Var(id=48) +1.Var(id=59) -1.Var(id=60) -1.Var(id=61) +1.Var(id=62) +4.Var(id=65) -4.Var(id=66) +1.Var(id=69) -1.Var(id=70) -1.Var(id=71) +1.Var(id=72) -1.Var(id=73) +1.Var(id=74) -2.Var(id=75) +2.Var(id=76) -1.Var(id=77) +1.Var(id=78) <= -1), Relation(-1.Var(id=1) +1.Var(id=2) -2.Var(id=3) +2.Var(id=4) +1.Var(id=9) -1.Var(id=10) -2.Var(id=13) +2.Var(id=14) -2.Var(id=17) +2.Var(id=18) +1.Var(id=19) -1.Var(id=20) +1.Var(id=23) -1.Var(id=24) +1.Var(id=27) -1.Var(id=28) +1.Var(id=33) -1.Var(id=34) -1.Var(id=37) +1.Var(id=38) +2.Var(id=39) -2.Var(id=40) +1.Var(id=43) -1.Var(id=44) -1.Var(id=53) +1.Var(id=54) -1.Var(id=57) +1.Var(id=58) -1.Var(id=61) +1.Var(id=62) +1.Var(id=77) -1.Var(id=78) +1.Var(id=79) -1.Var(id=80) +1.Var(id=81) -1.Var(id=82) <= -1), Relation(+1.Var(id=7) -1.Var(id=8) -1.Var(id=11) +1.Var(id=12) +1.Var(id=13) -1.Var(id=14) +1.Var(id=17) -1.Var(id=18) -1.Var(id=21) +1.Var(id=22) +1.Var(id=23) -1.Var(id=24) -1.Var(id=25) +1.Var(id=26) -1.Var(id=27) +1.Var(id=28) -1.Var(id=33) +1.Var(id=34) +1.Var(id=35) -1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=41) -1.Var(id=42) +1.Var(id=47) -1.Var(id=48) +1.Var(id=49) -1.Var(id=50) -1.Var(id=71) +1.Var(id=72) -2.Var(id=73) +2.Var(id=74) +1.Var(id=79) -1.Var(id=80) <= 0), Relation(-1.Var(id=9) +1.Var(id=10) -1.Var(id=15) +1.Var(id=16) -1.Var(id=17) +1.Var(id=18) -1.Var(id=19) +1.Var(id=20) +1.Var(id=21) -1.Var(id=22) +1.Var(id=37) -1.Var(id=38) +1.Var(id=41) -1.Var(id=42) +1.Var(id=49) -1.Var(id=50) +1.Var(id=51) -1.Var(id=52) +2.Var(id=53) -2.Var(id=54) +2.Var(id=59) -2.Var(id=60) -1.Var(id=61) +1.Var(id=62) +2.Var(id=73) -2.Var(id=74) -1.Var(id=75) +1.Var(id=76) +2.Var(id=83) -2.Var(id=84) -1.Var(id=85) +1.Var(id=86) <= 0), Relation(-1.Var(id=1) +1.Var(id=2) +2.Var(id=5) -2.Var(id=6) +2.Var(id=11) -2.Var(id=12) +1.Var(id=19) -1.Var(id=20) +1.Var(id=25) -1.Var(id=26) +1.Var(id=31) -1.Var(id=32) +1.Var(id=33) -1.Var(id=34) -1.Var(id=39) +1.Var(id=40) +2.Var(id=43) -2.Var(id=44) +1.Var(id=45) -1.Var(id=46) +1.Var(id=63) -1.Var(id=64) +1.Var(id=67) -1.Var(id=68) -1.Var(id=71) +1.Var(id=72) -1.Var(id=81) +1.Var(id=82) -1.Var(id=83) +1.Var(id=84) -2.Var(id=87) +2.Var(id=88) <= -1), Relation(-2.Var(id=5) +2.Var(id=6) +2.Var(id=7) -2.Var(id=8) +1.Var(id=9) -1.Var(id=10) +1.Var(id=11) -1.Var(id=12) -1.Var(id=15) +1.Var(id=16) -2.Var(id=29) +2.Var(id=30) +1.Var(id=37) -1.Var(id=38) +1.Var(id=45) -1.Var(id=46) -1.Var(id=51) +1.Var(id=52) +1.Var(id=57) -1.Var(id=58) +1.Var(id=59) -1.Var(id=60) -1.Var(id=69) +1.Var(id=70) +1.Var(id=73) -1.Var(id=74) +1.Var(id=75) -1.Var(id=76) -1.Var(id=79) +1.Var(id=80) +1.Var(id=81) -1.Var(id=82) <= 1), Relation(-1.Var(id=1) +1.Var(id=2) +1.Var(id=3) -1.Var(id=4) -1.Var(id=7) +1.Var(id=8) -2.Var(id=9) +2.Var(id=10) +1.Var(id=15) -1.Var(id=16) -1.Var(id=21) +1.Var(id=22) +1.Var(id=23) -1.Var(id=24) -1.Var(id=27) +1.Var(id=28) -1.Var(id=39) +1.Var(id=40) +1.Var(id=45) -1.Var(id=46) +1.Var(id=49) -1.Var(id=50) -1.Var(id=51) +1.Var(id=52) +1.Var(id=69) -1.Var(id=70) -1.Var(id=81) +1.Var(id=82) +2.Var(id=85) -2.Var(id=86) <= 0), Relation(+1.Var(id=1) -1.Var(id=2) -1.Var(id=9) +1.Var(id=10) +1.Var(id=13) -1.Var(id=14) -2.Var(id=17) +2.Var(id=18) -1.Var(id=23) +1.Var(id=24) -1.Var(id=27) +1.Var(id=28) -1.Var(id=29) +1.Var(id=30) -1.Var(id=51) +1.Var(id=52) +1.Var(id=63) -1.Var(id=64) +1.Var(id=65) -1.Var(id=66) -1.Var(id=67) +1.Var(id=68) +1.Var(id=69) -1.Var(id=70) +1.Var(id=79) -1.Var(id=80) -1.Var(id=81) +1.Var(id=82) <= 0), Relation(+1.Var(id=13) -1.Var(id=14) +1.Var(id=17) -1.Var(id=18) +1.Var(id=21) -1.Var(id=22) -1.Var(id=23) +1.Var(id=24) -1.Var(id=25) +1.Var(id=26) -1.Var(id=35) +1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=49) -1.Var(id=50) +1.Var(id=55) -1.Var(id=56) -2.Var(id=59) +2.Var(id=60) -1.Var(id=67) +1.Var(id=68) -1.Var(id=69) +1.Var(id=70) +1.Var(id=81) -1.Var(id=82) +1.Var(id=83) -1.Var(id=84) <= 0), Relation(-1.Var(id=3) +1.Var(id=4) +2.Var(id=7) -2.Var(id=8) -1.Var(id=9) +1.Var(id=10) +2.Var(id=25) -2.Var(id=26) +1.Var(id=31) -1.Var(id=32) +1.Var(id=35) -1.Var(id=36) -1.Var(id=39) +1.Var(id=40) -1.Var(id=47) +1.Var(id=48) -1.Var(id=59) +1.Var(id=60) +1.Var(id=63) -1.Var(id=64) -1.Var(id=75) +1.Var(id=76) +1.Var(id=85) -1.Var(id=86) +1.Var(id=89) -1.Var(id=90) <= 1), Relation(+1.Var(id=1) -1.Var(id=2) -1.Var(id=5) +1.Var(id=6) +1.Var(id=9) -1.Var(id=10) -1.Var(id=11) +1.Var(id=12) +1.Var(id=13) -1.Var(id=14) -1.Var(id=17) +1.Var(id=18) -1.Var(id=19) +1.Var(id=20) -2.Var(id=25) +2.Var(id=26) -1.Var(id=27) +1.Var(id=28) -1.Var(id=35) +1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=45) -1.Var(id=46) -1.Var(id=49) +1.Var(id=50) +1.Var(id=55) -1.Var(id=56) +1.Var(id=57) -1.Var(id=58) -1.Var(id=59) +1.Var(id=60) -1.Var(id=63) +1.Var(id=64) +1.Var(id=65) -1.Var(id=66) -2.Var(id=77) +2.Var(id=78) +1.Var(id=79) -1.Var(id=80) -1.Var(id=85) +1.Var(id=86) <= 0), Relation(-1.Var(id=3) +1.Var(id=4) -1.Var(id=5) +1.Var(id=6) -2.Var(id=7) +2.Var(id=8) +2.Var(id=11) -2.Var(id=12) -1.Var(id=13) +1.Var(id=14) -1.Var(id=17) +1.Var(id=18) +1.Var(id=21) -1.Var(id=22) -1.Var(id=23) +1.Var(id=24) +1.Var(id=33) -1.Var(id=34) -1.Var(id=39) +1.Var(id=40) -1.Var(id=43) +1.Var(id=44) -1.Var(id=47) +1.Var(id=48) +1.Var(id=49) -1.Var(id=50) -1.Var(id=53) +1.Var(id=54) +1.Var(id=55) -1.Var(id=56) +1.Var(id=61) -1.Var(id=62) -1.Var(id=67) +1.Var(id=68) -1.Var(id=83) +1.Var(id=84) +1.Var(id=85) -1.Var(id=86) +1.Var(id=89) -1.Var(id=90) <= -1), Relation(-1.Var(id=1) +1.Var(id=2) +1.Var(id=3) -1.Var(id=4) +1.Var(id=9) -1.Var(id=10) +1.Var(id=11) -1.Var(id=12) +1.Var(id=13) -1.Var(id=14) -2.Var(id=17) +2.Var(id=18) -1.Var(id=19) +1.Var(id=20) -1.Var(id=21) +1.Var(id=22) +1.Var(id=23) -1.Var(id=24) -2.Var(id=25) +2.Var(id=26) +1.Var(id=35) -1.Var(id=36) +1.Var(id=39) -1.Var(id=40) -1.Var(id=41) +1.Var(id=42) -1.Var(id=47) +1.Var(id=48) +1.Var(id=55) -1.Var(id=56) -1.Var(id=59) +1.Var(id=60) -1.Var(id=65) +1.Var(id=66) -1.Var(id=67) +1.Var(id=68) +2.Var(id=87) -2.Var(id=88) <= -1), Relation(-1.Var(id=1) +1.Var(id=2) +1.Var(id=5) -1.Var(id=6) -1.Var(id=9) +1.Var(id=10) +1.Var(id=21) -1.Var(id=22) -1.Var(id=23) +1.Var(id=24) -1.Var(id=27) +1.Var(id=28) -2.Var(id=31) +2.Var(id=32) +1.Var(id=33) -1.Var(id=34) +1.Var(id=35) -1.Var(id=36) +1.Var(id=37) -1.Var(id=38) -1.Var(id=39) +1.Var(id=40) +1.Var(id=55) -1.Var(id=56) -1.Var(id=57) +1.Var(id=58) -1.Var(id=79) +1.Var(id=80) -1.Var(id=83) +1.Var(id=84) +1.Var(id=87) -1.Var(id=88) <= 0), Relation(+1.Var(id=11) -1.Var(id=12) +1.Var(id=13) -1.Var(id=14) +1.Var(id=15) -1.Var(id=16) +1.Var(id=19) -1.Var(id=20) -1.Var(id=21) +1.Var(id=22) -2.Var(id=23) +2.Var(id=24) -1.Var(id=27) +1.Var(id=28) +1.Var(id=37) -1.Var(id=38) -1.Var(id=43) +1.Var(id=44) -1.Var(id=49) +1.Var(id=50) -1.Var(id=55) +1.Var(id=56) +2.Var(id=59) -2.Var(id=60) +1.Var(id=63) -1.Var(id=64) +1.Var(id=67) -1.Var(id=68) -1.Var(id=69) +1.Var(id=70) +1.Var(id=89) -1.Var(id=90) <= -1), Relation(-1.Var(id=7) +1.Var(id=8) +1.Var(id=11) -1.Var(id=12) -1.Var(id=21) +1.Var(id=22) -1.Var(id=25) +1.Var(id=26) +1.Var(id=29) -1.Var(id=30) -1.Var(id=31) +1.Var(id=32) -1.Var(id=37) +1.Var(id=38) -1.Var(id=39) +1.Var(id=40) -1.Var(id=45) +1.Var(id=46) -1.Var(id=51) +1.Var(id=52) -1.Var(id=55) +1.Var(id=56) -1.Var(id=69) +1.Var(id=70) -1.Var(id=73) +1.Var(id=74) +2.Var(id=79) -2.Var(id=80) -1.Var(id=89) +1.Var(id=90) <= 1), Relation(+1.Var(id=5) -1.Var(id=6) +2.Var(id=11) -2.Var(id=12) -1.Var(id=13) +1.Var(id=14) +1.Var(id=25) -1.Var(id=26) +4.Var(id=31) -4.Var(id=32) -1.Var(id=35) +1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=47) -1.Var(id=48) -1.Var(id=59) +1.Var(id=60) -1.Var(id=67) +1.Var(id=68) -1.Var(id=71) +1.Var(id=72) +1.Var(id=77) -1.Var(id=78) +1.Var(id=81) -1.Var(id=82) -1.Var(id=85) +1.Var(id=86) <= 0)]
[2024/08/19 16:43:01](INFO): Setup done. Proceeding to AST evaluation (backend: MTBDD).
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=2, automaton_id=0), operation_id=0, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=2, automaton_id=1), operation_id=1, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 2 and 2
[2024/08/19 16:43:01](INFO): Intersection done: result size=4, left operand size: 2 , right operand size: 2
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=2, automaton_id=0), operand2=AutomatonInfo(size=2, automaton_id=1), output=AutomatonInfo(size=4, automaton_id=2), operation_id=2, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=4, automaton_id=2), operand2=None, output=AutomatonInfo(size=3, automaton_id=3), operation_id=3, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 3 states, result 3.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=4, automaton_id=2), operand2=None, output=AutomatonInfo(size=3, automaton_id=4), operation_id=4, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 3, automaton_type=2)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=5, automaton_id=5), operation_id=5, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 3 and 5
[2024/08/19 16:43:01](INFO): Intersection done: result size=11, left operand size: 3 , right operand size: 5
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=3, automaton_id=4), operand2=AutomatonInfo(size=5, automaton_id=5), output=AutomatonInfo(size=11, automaton_id=6), operation_id=6, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=11, automaton_id=6), operand2=None, output=AutomatonInfo(size=14, automaton_id=7), operation_id=7, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 14 states, result 5.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=11, automaton_id=6), operand2=None, output=AutomatonInfo(size=5, automaton_id=8), operation_id=8, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 5, automaton_type=2)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=15, automaton_id=9), operation_id=9, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 5 and 15
[2024/08/19 16:43:01](INFO): Intersection done: result size=41, left operand size: 5 , right operand size: 15
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=5, automaton_id=8), operand2=AutomatonInfo(size=15, automaton_id=9), output=AutomatonInfo(size=41, automaton_id=10), operation_id=10, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=41, automaton_id=10), operand2=None, output=AutomatonInfo(size=61, automaton_id=11), operation_id=11, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 61 states, result 11.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=41, automaton_id=10), operand2=None, output=AutomatonInfo(size=11, automaton_id=12), operation_id=12, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 11, automaton_type=2)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=11, automaton_id=13), operation_id=13, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 11 and 11
[2024/08/19 16:43:01](INFO): Intersection done: result size=61, left operand size: 11 , right operand size: 11
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=11, automaton_id=12), operand2=AutomatonInfo(size=11, automaton_id=13), output=AutomatonInfo(size=61, automaton_id=14), operation_id=14, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=61, automaton_id=14), operand2=None, output=AutomatonInfo(size=79, automaton_id=15), operation_id=15, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 79 states, result 21.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=61, automaton_id=14), operand2=None, output=AutomatonInfo(size=21, automaton_id=16), operation_id=16, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=17, automaton_id=17), operation_id=17, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 17
[2024/08/19 16:43:02](INFO): Intersection done: result size=115, left operand size: 21 , right operand size: 17
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=16), operand2=AutomatonInfo(size=17, automaton_id=17), output=AutomatonInfo(size=115, automaton_id=18), operation_id=18, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=115, automaton_id=18), operand2=None, output=AutomatonInfo(size=159, automaton_id=19), operation_id=19, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 159 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=115, automaton_id=18), operand2=None, output=AutomatonInfo(size=21, automaton_id=20), operation_id=20, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=3, automaton_id=21), operation_id=21, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 3
[2024/08/19 16:43:02](INFO): Intersection done: result size=47, left operand size: 21 , right operand size: 3
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=20), operand2=AutomatonInfo(size=3, automaton_id=21), output=AutomatonInfo(size=47, automaton_id=22), operation_id=22, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=47, automaton_id=22), operand2=None, output=AutomatonInfo(size=45, automaton_id=23), operation_id=23, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 45 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=47, automaton_id=22), operand2=None, output=AutomatonInfo(size=21, automaton_id=24), operation_id=24, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=7, automaton_id=25), operation_id=25, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 7
[2024/08/19 16:43:02](INFO): Intersection done: result size=47, left operand size: 21 , right operand size: 7
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=24), operand2=AutomatonInfo(size=7, automaton_id=25), output=AutomatonInfo(size=47, automaton_id=26), operation_id=26, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=47, automaton_id=26), operand2=None, output=AutomatonInfo(size=34, automaton_id=27), operation_id=27, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 34 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=47, automaton_id=26), operand2=None, output=AutomatonInfo(size=21, automaton_id=28), operation_id=28, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=3, automaton_id=29), operation_id=29, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 3
[2024/08/19 16:43:02](INFO): Intersection done: result size=43, left operand size: 21 , right operand size: 3
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=28), operand2=AutomatonInfo(size=3, automaton_id=29), output=AutomatonInfo(size=43, automaton_id=30), operation_id=30, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=43, automaton_id=30), operand2=None, output=AutomatonInfo(size=26, automaton_id=31), operation_id=31, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 26 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=43, automaton_id=30), operand2=None, output=AutomatonInfo(size=21, automaton_id=32), operation_id=32, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=11, automaton_id=33), operation_id=33, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 11
[2024/08/19 16:43:02](INFO): Intersection done: result size=31, left operand size: 21 , right operand size: 11
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=32), operand2=AutomatonInfo(size=11, automaton_id=33), output=AutomatonInfo(size=31, automaton_id=34), operation_id=34, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=31, automaton_id=34), operand2=None, output=AutomatonInfo(size=39, automaton_id=35), operation_id=35, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 39 states, result 0.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=31, automaton_id=34), operand2=None, output=AutomatonInfo(size=0, automaton_id=36), operation_id=36, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 0, automaton_type=2)
[2024/08/19 16:43:02](INFO): The SAT value of the result automaton is unsat
unsat

Following the corresponding query in the SMT-LIB format: v45_problem_2__003.smt2.slack.smt2.txt.

Best regards, Nicolas

[MichalHe]

Hi @nicolasAmat, thank you for letting me know, and sorry for taking a long time to respond - I missed that a new issue has been submitted.

You have configured Amaya correctly. There are numerous things that might have gone wrong inside Amaya. My suspicion is that there might be a problem somewhere in the preprocessing heuristics, but I have not checked these fully.

I will definitely fix the problem and let you know.

Thank you for trying out Amaya. Take care, Michal.