// Purpose: tests that groups of integers can be reasoned about with finite quantifiers
// Description: A single module, which declares a group of integers 0, 1, 2, and 3. The module has two properties: the first property uses a finite_exists quantifier to assert that there exists a member of the group less than 2. The second property uses a finite_exists quantifier to assert that there exists a member of the group greater than 3. The properties are checked with bmc(0).
// Expectation: The first property should fail, the second should pass.
// Validation: removing FiniteQuantsExpander from UclidMain.scala will cause an error on the solver side. inserting a bug into FiniteQuantsExpander will cause an error.


module main {
    group myGroup : integer = {0, 1, 2, 3};

    property test1 : finite_exists (int : integer) in myGroup :: int < 2; //Should pass
    property test2 : finite_exists (int : integer) in myGroup :: int > 3; //Should fail

    init {
    }

    next {
    }

    control {
        v = unroll(0);
        check;
        print_results;
    }
}
